| .. |
|
Compiler
|
feat: prevent adversarial users from using hugeFuel in actual code
|
2020-01-11 15:34:39 -08:00 |
|
Data
|
feat: file IO using handles
|
2020-01-12 08:02:48 -08:00 |
|
Elab
|
fix: missing file
|
2020-01-13 16:52:12 -08:00 |
|
EqnCompiler
|
|
|
|
Meta
|
doc: try naming result type
|
2020-01-14 08:49:41 -08:00 |
|
Parser
|
feat: add ParserDescrCore.tacticSymbol constructor
|
2020-01-13 16:54:52 -08:00 |
|
Util
|
feat: catch deep recursion at MetaM, TermElabM and CommandElabM
|
2020-01-11 15:03:58 -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
|
feat: enable leadingIdentAsSymbol for tactic category
|
2020-01-13 16:20:34 -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
|
fix: elaboration of macro-generated defs
|
2020-01-12 10:32:27 -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
|
chore: naming convention
|
2019-12-15 18:28:00 -08:00 |
|
Message.lean
|
chore: move Message to Lean
|
2020-01-10 10:58:50 -08:00 |
|
Meta.lean
|
feat: add kabstract
|
2020-01-10 13:10:03 -08:00 |
|
MetavarContext.lean
|
feat: elabDefLike
|
2020-01-06 12:10:08 -08:00 |
|
Modifiers.lean
|
|
|
|
Parser.lean
|
feat: add tactic parser attributes
|
2020-01-13 13:00:19 -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
|
chore: make Syntax.reprint output without source info more readable
|
2020-01-12 10:32:27 -08:00 |
|
ToExpr.lean
|
chore: remove mkCApp* functions
|
2019-12-04 13:07:42 -08:00 |
