lean4-htt/src/Lean
2020-07-13 16:22:48 -07:00
..
Compiler chore: move RBTree and RBMap to Std 2020-06-25 13:26:16 -07:00
Data chore: move RBTree and RBMap to Std 2020-06-25 13:26:16 -07:00
Elab feat: add CtorView and modifier validation for inductive and constructors 2020-07-13 16:22:48 -07:00
EqnCompiler chore: remove prelude commands from Lean package 2020-06-25 11:21:17 -07:00
Meta feat: add instantiateForall 2020-07-11 08:01:36 -07:00
Parser feat: add declModifiers to constructor declarations 2020-07-13 16:22:48 -07:00
PrettyPrinter chore: remove prelude commands from Lean package 2020-06-25 11:21:17 -07:00
Util chore: move PersistentArray to Std 2020-06-25 13:02:21 -07:00
Attributes.lean chore: move HashMap and HashSet to Std 2020-06-25 12:46:56 -07:00
AuxRecursor.lean chore: remove prelude commands from Lean package 2020-06-25 11:21:17 -07:00
Class.lean chore: remove prelude commands from Lean package 2020-06-25 11:21:17 -07:00
Compiler.lean chore: remove prelude commands from Lean package 2020-06-25 11:21:17 -07:00
Declaration.lean chore: remove prelude commands from Lean package 2020-06-25 11:21:17 -07:00
Delaborator.lean chore: move RBTree and RBMap to Std 2020-06-25 13:26:16 -07:00
Elab.lean feat: add Inductive.lean 2020-06-26 12:44:13 -07:00
Environment.lean fix: freeing Environments in tests 2020-07-10 07:42:26 -07:00
EqnCompiler.lean chore: remove prelude commands from Lean package 2020-06-25 11:21:17 -07:00
Eval.lean chore: remove prelude commands from Lean package 2020-06-25 11:21:17 -07:00
Expr.lean feat: add Expr.inferImplicit 2020-07-13 16:22:48 -07:00
HeadIndex.lean chore: remove prelude commands from Lean package 2020-06-25 11:21:17 -07:00
Hygiene.lean chore: remove prelude commands from Lean package 2020-06-25 11:21:17 -07:00
KeyedDeclsAttribute.lean chore: remove prelude commands from Lean package 2020-06-25 11:21:17 -07:00
Level.lean chore: move HashMap and HashSet to Std 2020-06-25 12:46:56 -07:00
Linter.lean chore: remove prelude commands from Lean package 2020-06-25 11:21:17 -07:00
LocalContext.lean chore: move PersistentArray to Std 2020-06-25 13:02:21 -07:00
Message.lean chore: move PersistentArray to Std 2020-06-25 13:02:21 -07:00
Meta.lean chore: remove prelude commands from Lean package 2020-06-25 11:21:17 -07:00
MetavarContext.lean chore: move HashMap and HashSet to Std 2020-06-25 12:46:56 -07:00
Modifiers.lean chore: remove prelude commands from Lean package 2020-06-25 11:21:17 -07:00
Parser.lean chore: remove prelude commands from Lean package 2020-06-25 11:21:17 -07:00
PrettyPrinter.lean chore: remove prelude commands from Lean package 2020-06-25 11:21:17 -07:00
ProjFns.lean chore: remove prelude commands from Lean package 2020-06-25 11:21:17 -07:00
ReducibilityAttrs.lean chore: remove prelude commands from Lean package 2020-06-25 11:21:17 -07:00
Runtime.lean chore: remove prelude commands from Lean package 2020-06-25 11:21:17 -07:00
Scopes.lean chore: remove prelude commands from Lean package 2020-06-25 11:21:17 -07:00
Structure.lean chore: remove prelude commands from Lean package 2020-06-25 11:21:17 -07:00
Syntax.lean chore: remove prelude commands from Lean package 2020-06-25 11:21:17 -07:00
ToExpr.lean chore: remove prelude commands from Lean package 2020-06-25 11:21:17 -07:00
Util.lean chore: remove prelude commands from Lean package 2020-06-25 11:21:17 -07:00