max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/src/Lean/Meta/Match
History
Leonardo de Moura b1e52f1475
chore: mark Meta.Context.config as private (#6051) 
Motivation: we want to modify the internal representation and improve
`isDefEq` caching.
This PR is preparing the stage for future modifications.
2024-11-13 13:30:06 +11:00
..
MatcherApp chore: mark Meta.Context.config as private (#6051) 2024-11-13 13:30:06 +11:00
Basic.lean chore: move MessageData.ofConstName earlier (#5877) 2024-10-29 21:23:51 +00:00
CaseArraySizes.lean feat: change Array.get to take a Nat and a proof (#6032) 2024-11-12 03:30:46 +00:00
CaseValues.lean fix: match literal pattern support 2024-02-24 16:08:07 -08:00
Match.lean feat: change Array.get to take a Nat and a proof (#6032) 2024-11-12 03:30:46 +00:00
MatchEqs.lean feat: change Array.get to take a Nat and a proof (#6032) 2024-11-12 03:30:46 +00:00
MatchEqsExt.lean fix: do not include internal match equational theorems at simp trace (#4274) 2024-05-25 17:16:19 +00:00
MatcherApp.lean refactor: module MatcherApp.Transform (#3439) 2024-02-22 16:16:26 +00:00
MatcherInfo.lean refactor: generalize addMatcherInfo (#5068) 2024-08-16 06:24:32 +00:00
MatchPatternAttr.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
MVarRenaming.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
Value.lean fix: match literal pattern support 2024-02-24 16:08:07 -08:00