max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/src/Init/Lean/Meta
History
Leonardo de Moura 81278c1509 feat: add instanceExtension 
Use discrimination trees indexing type class instances.
2019-11-26 17:01:36 -08:00
..
Basic.lean feat: add instanceExtension 2019-11-26 17:01:36 -08:00
Check.lean feat: ensure trace messages at MetaM save Environment, MetavarContext, and LocalContext 2019-11-22 11:50:19 -08:00
DiscrTree.lean feat: break insert into two steps 2019-11-26 17:01:36 -08:00
Exception.lean
ExprDefEq.lean feat: use isProofQuick to implement isDefEqProofIrrel 2019-11-25 08:42:23 -08:00
FunInfo.lean chore: remove ParamInfo.proof field 2019-11-25 08:42:23 -08:00
InferType.lean fix: typo 2019-11-25 15:53:08 -08:00
Instances.lean feat: add instanceExtension 2019-11-26 17:01:36 -08:00
LevelDefEq.lean feat: ensure trace messages at MetaM save Environment, MetavarContext, and LocalContext 2019-11-22 11:50:19 -08:00
Offset.lean
Reduce.lean feat: add reduce 2019-11-25 08:42:23 -08:00
WHNF.lean