| .. |
|
Compiler
|
feat: prevent adversarial users from using hugeFuel in actual code
|
2020-01-11 15:34:39 -08:00 |
|
Data
|
refactor: move declarations used at macro command to LeanInit
|
2020-01-15 20:53:23 -08:00 |
|
Elab
|
feat: add eval for seq and assumption
|
2020-01-16 17:04:21 -08:00 |
|
EqnCompiler
|
|
|
|
Meta
|
fix: typos
|
2020-01-16 19:28:49 -08:00 |
|
Parser
|
feat: allow underscore to be used as identifier
|
2020-01-16 17:51:01 -08:00 |
|
Util
|
feat: display goal when tactic fails
|
2020-01-16 19:23:02 -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
|
chore: avoid ^do ...
|
2019-12-11 06:19: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
|
refactor: move MonadQuotation to LeanInit, add MacroM
|
2020-01-15 20:53:23 -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: add instantiateLCtxMVars and instantiateMVarDeclMVars
|
2020-01-16 15:45:40 -08:00 |
|
Message.lean
|
feat: add ppGoal
|
2020-01-16 19:16:06 -08:00 |
|
Meta.lean
|
feat: add kabstract
|
2020-01-10 13:10:03 -08:00 |
|
MetavarContext.lean
|
feat: add instantiateLCtxMVars and instantiateMVarDeclMVars
|
2020-01-16 15:45:40 -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 declarations used at macro command to LeanInit
|
2020-01-15 20:53:23 -08:00 |
|
ToExpr.lean
|
chore: remove mkCApp* functions
|
2019-12-04 13:07:42 -08:00 |
