Commit 2023-11-17 21:01 0847db54

View on Github →

feat: convenient meta declarations (#7519) These declarations are picked from #5938.

Estimated changes

Modified Mathlib/Lean/Expr/Basic.lean

added def Lean.Expr.getAppApps

added def Lean.Expr.reduceProjStruct?

Modified Mathlib/Lean/Meta/Basic.lean

added def Lean.Meta.mkRel

added def Lean.Meta.pureIsDefEq

Modified Mathlib/Tactic/Relation/Rfl.lean

added def Lean.Expr.relSidesIfRefl?

Modified Mathlib/Tactic/Relation/Symm.lean

added def Lean.Expr.relSidesIfSymm?

Created test/meta.lean

added def Tests.eFalse

added def Tests.eNat

added def Tests.eNatOne

added def Tests.eNatZero

added def Tests.eTrue

added def Tests.eq2

added theorem Tests.eq2_symm