Commit 2024-09-23 21:06 3b440125
View on Github →feat: The computable functions are closed under if-then-else definitions with computable predicates (#17039) As discussed at https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/by.20decide.20implies.20Computable/near/471964724