Commit 2024-02-26 01:48 fb56e88b

View on Github →

chore: cleanup proof of Nat.Partrec.Code.rec_prim (#10978) This is in preparation for a fix to be performed on nightly-testing. It restores the proof structure to something more similar to the original lean 3 proof.

Estimated changes