| .. |
|
Deriving
|
feat: add deriving Repr
|
2020-12-18 14:19:43 -08:00 |
|
PreDefinition
|
feat: add throwMVarError!
|
2020-12-25 10:03:42 -08:00 |
|
Quotation
|
perf: let*-bind syntax match RHSs before duplicating them
|
2020-12-22 17:25:46 +01:00 |
|
Tactic
|
chore: remove <or>, first subsumes it
|
2020-12-22 14:10:08 -08:00 |
|
App.lean
|
chore: use deriving Inhabited
|
2020-12-13 10:09:20 -08:00 |
|
Attributes.lean
|
refactor: move to attr syntax category
|
2020-12-15 20:22:04 -08:00 |
|
AutoBound.lean
|
feat: extend valid set of valid auto bound names
|
2020-12-19 12:36:19 -08:00 |
|
Binders.lean
|
refactor: use quotations & implicit token positions from getRef to clean up a bit
|
2020-12-21 17:32:36 +01:00 |
|
BuiltinNotation.lean
|
chore: adapt stdlib to new antiquotation splices
|
2020-12-12 17:20:03 +01:00 |
|
CollectFVars.lean
|
chore: cleanup
|
2020-10-26 07:42:08 -07:00 |
|
Command.lean
|
feat: add throwMVarError!
|
2020-12-25 10:03:42 -08:00 |
|
Declaration.lean
|
feat: add optional (priority := <prio>) to instance command
|
2020-12-21 10:02:12 -08:00 |
|
DeclModifiers.lean
|
feat: expand macros in attributes eagerly
|
2020-12-15 15:11:19 -08:00 |
|
DeclUtil.lean
|
feat: improve type mismatch error messages
|
2020-12-17 07:11:52 -08:00 |
|
DefView.lean
|
feat: add optional (priority := <prio>) to instance command
|
2020-12-21 10:02:12 -08:00 |
|
Deriving.lean
|
feat: add deriving Repr
|
2020-12-18 14:19:43 -08:00 |
|
Do.lean
|
fix: position of failed to synthesize toStream ... error
|
2020-12-25 10:03:42 -08:00 |
|
Exception.lean
|
feat: add throwMVarError!
|
2020-12-25 10:03:42 -08:00 |
|
Frontend.lean
|
feat: parser: store options & pass to evalConst
|
2020-12-16 23:15:58 +01:00 |
|
Import.lean
|
chore: cleanup
|
2020-10-26 07:54:11 -07:00 |
|
Inductive.lean
|
refactor: add MonadError class abbreviation
|
2020-12-14 09:15:26 -08:00 |
|
LetRec.lean
|
feat: add throwMVarError!
|
2020-12-25 10:03:42 -08:00 |
|
Level.lean
|
fix: bug introduced when moving to new frontend
|
2020-12-21 07:34:48 -08:00 |
|
Log.lean
|
feat: add throwMVarError!
|
2020-12-25 10:03:42 -08:00 |
|
Match.lean
|
fix: error message and test
|
2020-12-25 10:03:42 -08:00 |
|
MutualDef.lean
|
refactor: use quotations & implicit token positions from getRef to clean up a bit
|
2020-12-21 17:32:36 +01:00 |
|
PreDefinition.lean
|
chore: remove #lang lean4 header
|
2020-10-25 09:54:07 -07:00 |
|
Print.lean
|
fix: avoid macro scopes in error message
|
2020-12-11 11:23:44 -08:00 |
|
Quotation.lean
|
feat: lift restriction on number of antiquotations in splice
|
2020-12-25 18:41:03 +01:00 |
|
StructInst.lean
|
feat: improve {...} error message
|
2020-12-24 09:35:55 -08:00 |
|
Structure.lean
|
feat: modify structSimpleBinder parser
|
2020-12-23 08:23:14 -08:00 |
|
Syntax.lean
|
fix: name resolution at syntax command
|
2020-12-22 08:40:00 -08:00 |
|
SyntheticMVars.lean
|
feat: add throwMVarError!
|
2020-12-25 10:03:42 -08:00 |
|
Tactic.lean
|
chore: remove #lang lean4 header
|
2020-10-25 09:54:07 -07:00 |
|
Term.lean
|
fix: error message and test
|
2020-12-25 10:03:42 -08:00 |
|
Util.lean
|
feat: add optional (priority := <prio>) to instance command
|
2020-12-21 10:02:12 -08:00 |
