mathlib3
a859f10d - refactor(computability/primrec): simpler proof of `primrec.of_equiv` (#5905)

Commit

4 years ago

refactor(computability/primrec): simpler proof of `primrec.of_equiv` (#5905) 12X smaller proof term co-authors: `lean-gptf`, Stanislas Polu

Author

Jesse Michael Han

Parents