lean4-htt/src/Lean/Meta/Sym
Leonardo de Moura af438425d5
perf: avoid mkAppM in Sym.simp (#12099)
This PR ensures `Sym.simpGoal` does not use `mkAppM`. It also increases
the default number of maximum steps in `Sym.simp`.
2026-01-22 00:01:43 +00:00
..
Simp perf: avoid mkAppM in Sym.simp (#12099) 2026-01-22 00:01:43 +00:00
AbstractS.lean refactor: reorganize SymM and GrindM monad hierarchy (#11909) 2026-01-06 01:12:07 +00:00
AlphaShareBuilder.lean feat: add simpControl simproc for if-then-else simplification (#12035) 2026-01-18 04:14:26 +00:00
AlphaShareCommon.lean refactor: reorganize SymM and GrindM monad hierarchy (#11909) 2026-01-06 01:12:07 +00:00
Apply.lean feat: metavar cleanup in Sym.simp (#12096) 2026-01-21 21:36:17 +00:00
ExprPtr.lean refactor: reorganize SymM and GrindM monad hierarchy (#11909) 2026-01-06 01:12:07 +00:00
InferType.lean refactor: reorganize SymM and GrindM monad hierarchy (#11909) 2026-01-06 01:12:07 +00:00
InstantiateMVarsS.lean refactor: reorganize SymM and GrindM monad hierarchy (#11909) 2026-01-06 01:12:07 +00:00
InstantiateS.lean perf: replaceS and instantiateRevBetaS (#11911) 2026-01-06 03:03:01 +00:00
Intro.lean refactor: reorganize SymM and GrindM monad hierarchy (#11909) 2026-01-06 01:12:07 +00:00
IsClass.lean feat: intro tactic for SymM (#11803) 2025-12-26 03:45:33 +00:00
LitValues.lean feat: String and Char simprocs for SymM (#12077) 2026-01-21 00:05:40 +00:00
LooseBVarsS.lean refactor: reorganize SymM and GrindM monad hierarchy (#11909) 2026-01-06 01:12:07 +00:00
MaxFVar.lean chore: Sym cleanup (#11833) 2025-12-29 17:07:56 +00:00
Offset.lean feat: offset terms in Sym (#12053) 2026-01-20 04:57:52 +00:00
Pattern.lean feat: metavar cleanup in Sym.simp (#12096) 2026-01-21 21:36:17 +00:00
ProofInstInfo.lean feat: metavar cleanup in Sym.simp (#12096) 2026-01-21 21:36:17 +00:00
ReplaceS.lean perf: replaceS and instantiateRevBetaS (#11911) 2026-01-06 03:03:01 +00:00
Simp.lean chore: normalize Sym APIs (#12088) 2026-01-21 17:02:22 +00:00
SymM.lean refactor: reorganize SymM and GrindM monad hierarchy (#11909) 2026-01-06 01:12:07 +00:00
Util.lean feat: checkMaxShared (#12083) 2026-01-21 14:55:46 +00:00