Def Lean.Meta.preservingMCtx

Modification history

2024-07-19 05:13

Mathlib/Lean/Meta/Basic.lean

chore(Mathlib/Lean): remove use of autoImplicit (#14884) …

Modified Lean.Meta.preservingMCtx View on Github →

2023-04-18 12:01

Mathlib/Lean/Meta/Basic.lean

feat: `propose`, a forwards-reasoning analogue of `library_search`. (#2898) …

Added Lean.Meta.preservingMCtx View on Github →