Commit 2023-05-01 22:19 31dba13a

View on Github →

feat: make Acc.rec and many related defs computable (#3535) Lean 4 code generator has had no native supports for Acc.rec. This PR makes Acc.rec computable. This change makes many defs computable. Especially, computable PFun.fix and Part.hasFix enables us to reason about partial functions. This PR also renames some instances and gives PFun.lift @[coe] attr.

Estimated changes

Modified Mathlib/Computability/TuringMachine.lean

added def Turing.TM0.eval

added def Turing.TM1.eval

added def Turing.TM2.eval

added def Turing.eval

added def Turing.evalInduction

Modified Mathlib/Control/Fix.lean

Modified Mathlib/Control/LawfulFix.lean

Modified Mathlib/Data/Finset/PImage.lean

added def Finset.pimage

Modified Mathlib/Data/PFun.lean

added def PFun.fix

added def PFun.fixInduction'

added def PFun.fixInduction

Modified Mathlib/Init/Data/Nat/Lemmas.lean

Modified Mathlib/Init/Logic.lean

deleted def WellFounded.fix'

Modified Mathlib/Order/GameAdd.lean

added def Prod.GameAdd.fix

added def Sym2.GameAdd.fix

Modified lake-manifest.json