| .. |
|
Compiler
|
fix: put limit on Nat.pow constant folding
|
2020-01-21 09:16:38 -08:00 |
|
Data
|
fix: syntax: do not qualify fresh kinds
|
2020-01-20 14:58:58 -08:00 |
|
Elab
|
fix: use nonReservedSymbol when defining tactic new syntax
|
2020-01-21 14:37:29 -08:00 |
|
EqnCompiler
|
|
|
|
Meta
|
feat: eval apply tactic
|
2020-01-19 16:23:32 -08:00 |
|
Parser
|
feat: add antiquotation support for strLit, numLit and charLit
|
2020-01-22 12:57:28 -08:00 |
|
Util
|
feat: add findMVar?
|
2020-01-19 16:03:01 -08:00 |
|
Attributes.lean
|
feat: declare_syntax_cat without importing Init.Lean
|
2020-01-11 09:02:50 -08:00 |
|
AuxRecursor.lean
|
|
|
|
Class.lean
|
refactor: registerAttribute ==> registerBuiltinAttribute
|
2020-01-10 17:08:12 -08:00 |
|
Compiler.lean
|
|
|
|
Declaration.lean
|
fix: missing isUnsafe fieldat OpaqueVal
|
2019-12-30 11:53:08 -08:00 |
|
Elab.lean
|
refactor: add Elab/Syntax.lean
|
2020-01-14 14:22:55 -08:00 |
|
Environment.lean
|
chore: remove unnecessary argument
|
2020-01-01 09:19:00 -08:00 |
|
EqnCompiler.lean
|
|
|
|
Eval.lean
|
feat: override standard streams
|
2020-01-19 17:23:12 -08:00 |
|
Expr.lean
|
feat: add support for optParam
|
2020-01-06 16:41:48 -08:00 |
|
HeadIndex.lean
|
feat: add HeadIndex
|
2020-01-10 11:58:22 -08:00 |
|
Hygiene.lean
|
feat: add Syntax.identToAtom
|
2020-01-21 13:25:20 -08:00 |
|
Level.lean
|
feat: add LevelSet and PersistentLevelSet
|
2020-01-05 13:26:25 -08:00 |
|
Linter.lean
|
chore: move Message to Lean
|
2020-01-10 10:58:50 -08:00 |
|
LocalContext.lean
|
feat: extract macro scopes at getUnusedName
|
2020-01-18 15:51:54 -08:00 |
|
Message.lean
|
feat: add MessageData.ofGoal
|
2020-01-16 20:22:38 -08:00 |
|
Meta.lean
|
feat: add kabstract
|
2020-01-10 13:10:03 -08:00 |
|
MetavarContext.lean
|
fix: tag refine subgoals
|
2020-01-19 11:58:17 -08:00 |
|
Modifiers.lean
|
|
|
|
Parser.lean
|
feat: add syntax category
|
2020-01-14 12:34:45 -08:00 |
|
ProjFns.lean
|
chore: naming convention
|
2019-12-15 07:48:42 -08:00 |
|
ReducibilityAttrs.lean
|
|
|
|
Runtime.lean
|
|
|
|
Scopes.lean
|
|
|
|
Structure.lean
|
chore: naming convention
|
2019-12-15 07:48:42 -08:00 |
|
Syntax.lean
|
refactor: move Syntax helper functions to LeanInit
|
2020-01-22 12:58:06 -08:00 |
|
ToExpr.lean
|
chore: remove mkCApp* functions
|
2019-12-04 13:07:42 -08:00 |
