| .. |
|
Compiler
|
fix: Borrow.lean
|
2019-12-22 19:20:42 -08:00 |
|
Data
|
chore: naming convention
|
2019-12-15 18:28:00 -08:00 |
|
Elab
|
feat: elaborate sortApp
|
2019-12-30 11:00:13 -08:00 |
|
EqnCompiler
|
chore: library/Init ==> src/Init
|
2019-11-22 06:06:05 -08:00 |
|
Meta
|
chore: combine MessageData.context + MessageData.withOptions into MessageData.context
|
2019-12-22 09:15:04 -08:00 |
|
Parser
|
fix: raise precedence inside antiquotation parser
|
2019-12-30 08:24:29 -08:00 |
|
Util
|
refactor: trace directly to MessageLog at Elab monads
|
2019-12-22 09:58:31 -08:00 |
|
Attributes.lean
|
chore: naming convention
|
2019-12-15 18:28:00 -08:00 |
|
AuxRecursor.lean
|
chore: library/Init ==> src/Init
|
2019-11-22 06:06:05 -08:00 |
|
Class.lean
|
chore: naming convention
|
2019-12-15 18:28:00 -08:00 |
|
Compiler.lean
|
chore: library/Init ==> src/Init
|
2019-11-22 06:06:05 -08:00 |
|
Declaration.lean
|
fix: missing isUnsafe fieldat OpaqueVal
|
2019-12-30 11:53:08 -08:00 |
|
Elab.lean
|
refactor: split Elab/Term.lean into smaller files
|
2019-12-19 07:26:54 -08:00 |
|
Environment.lean
|
feat: expose evalConst
|
2019-12-30 11:41:36 -08:00 |
|
EqnCompiler.lean
|
chore: library/Init ==> src/Init
|
2019-11-22 06:06:05 -08:00 |
|
Eval.lean
|
chore: avoid ^do ...
|
2019-12-11 06:19:12 -08:00 |
|
Expr.lean
|
fix: leaks
|
2019-12-22 15:09:19 -08:00 |
|
Hygiene.lean
|
refactor: simplify MacroHygiene implementations
|
2019-12-20 14:19:09 +01:00 |
|
Level.lean
|
fix: typo
|
2019-12-29 09:49:55 -08:00 |
|
Linter.lean
|
chore: move helper modules to src/Init/Lean/Util
|
2019-12-04 17:17:34 -08:00 |
|
LocalContext.lean
|
chore: naming convention
|
2019-12-15 18:28:00 -08:00 |
|
Meta.lean
|
feat: add user-friendly Meta.Exception -> MessageData
|
2019-12-10 15:49:52 -08:00 |
|
MetavarContext.lean
|
feat: implement design documented at 868a217202
|
2019-12-21 15:53:36 -08:00 |
|
Modifiers.lean
|
chore: library/Init ==> src/Init
|
2019-11-22 06:06:05 -08:00 |
|
Parser.lean
|
chore: library/Init ==> src/Init
|
2019-11-22 06:06:05 -08:00 |
|
ProjFns.lean
|
chore: naming convention
|
2019-12-15 07:48:42 -08:00 |
|
ReducibilityAttrs.lean
|
chore: library/Init ==> src/Init
|
2019-11-22 06:06:05 -08:00 |
|
Runtime.lean
|
chore: library/Init ==> src/Init
|
2019-11-22 06:06:05 -08:00 |
|
Scopes.lean
|
chore: library/Init ==> src/Init
|
2019-11-22 06:06:05 -08:00 |
|
Structure.lean
|
chore: naming convention
|
2019-12-15 07:48:42 -08:00 |
|
Syntax.lean
|
feat: support ident antiquotations (inside term parsers, for now)
|
2019-12-30 08:24:29 -08:00 |
|
ToExpr.lean
|
chore: remove mkCApp* functions
|
2019-12-04 13:07:42 -08:00 |
