Leonardo de Moura
|
960e964b71
|
feat: allow user to "erase" [simp] lemmas
|
2021-03-04 11:36:12 -08:00 |
|
Leonardo de Moura
|
bb2ca97df9
|
refactor: add options for controlling whether variables are included or not at mkLambdaFVars and mkForallFVars
|
2021-02-17 13:49:27 -08:00 |
|
Leonardo de Moura
|
ea0fda39bc
|
chore: Declaration.lean naming convention
`Declaration.lean` was one of the first Lean 4 files, and was still
using an old naming convention.
cc @Kha
|
2021-01-20 17:07:02 -08:00 |
|
Leonardo de Moura
|
b6bb31a131
|
feat: "compile" 'extern' axioms
|
2021-01-13 09:43:25 -08:00 |
|
Leonardo de Moura
|
84f78edb31
|
feat: store declaration ranges
|
2021-01-11 12:50:11 -08:00 |
|
Leonardo de Moura
|
308c61027a
|
feat: save doc strings
We can now document `let rec` too.
|
2021-01-10 07:13:33 -08:00 |
|
Leonardo de Moura
|
4fc06bfcca
|
feat: add optional (priority := <prio>) to instance command
|
2020-12-21 10:02:12 -08:00 |
|
Leonardo de Moura
|
0bbc2ca884
|
feat: elaborate optDeriving
|
2020-12-13 09:05:03 -08:00 |
|
Leonardo de Moura
|
fdc2c9f281
|
feat: process local instance ... and scoped instance ... commands
|
2020-12-05 15:46:25 -08:00 |
|
Leonardo de Moura
|
10102bf370
|
chore: remove "local" before attribute command
`local` is now part of the `Term.attrInstance` parser.
|
2020-12-05 07:47:28 -08:00 |
|
Leonardo de Moura
|
9389bca624
|
feat: elaborate attrKind
|
2020-12-05 07:40:55 -08:00 |
|
Leonardo de Moura
|
f67c93191f
|
feat: use |>.
|
2020-11-19 08:38:47 -08:00 |
|
Leonardo de Moura
|
0fcf6217ec
|
feat: optional := before constructors in the inductive command
@Kha In the documentation, I will always use `:=`. The idea is to
avoid the issue: why does `structure` have a `:=` but `inductive`
doesn't.
|
2020-11-19 06:43:14 -08:00 |
|
Leonardo de Moura
|
70385b87fa
|
feat: add instance MonadRef MacroM
|
2020-11-13 16:00:31 -08:00 |
|
Leonardo de Moura
|
f17e226638
|
chore: naming convention
Example: `mkNameStr` => `Name.mkStr`
cc @Kha
|
2020-11-11 10:08:55 -08:00 |
|
Leonardo de Moura
|
2d2d39c78e
|
chore: use mut
|
2020-11-07 17:32:13 -08:00 |
|
Leonardo de Moura
|
13c2a8ff51
|
chore: remove #lang lean4 header
|
2020-10-25 09:54:07 -07:00 |
|
Leonardo de Moura
|
93a8bb737f
|
chore: cleanup
|
2020-10-21 11:07:18 -07:00 |
|
Leonardo de Moura
|
bed3dd61f0
|
feat: expand builtin_initialize
|
2020-10-19 15:09:46 -07:00 |
|
Leonardo de Moura
|
3cfff9df14
|
chore: remove workarounds
|
2020-10-15 15:34:36 -07:00 |
|
Leonardo de Moura
|
d1ad5eb51a
|
chore: add workarounds
|
2020-10-15 14:56:38 -07:00 |
|
Leonardo de Moura
|
43efdd50f7
|
chore: move to new frontend
|
2020-10-14 17:38:17 -07:00 |
|
Leonardo de Moura
|
b7658ef91f
|
chore: move to new frontend
|
2020-10-13 17:11:52 -07:00 |
|
Leonardo de Moura
|
fa6b7b6393
|
feat: add MonadResolveName type class
`AttrM` can now resolve names.
|
2020-10-10 11:33:52 -07:00 |
|
Leonardo de Moura
|
63edecf106
|
feat: expand initialize macro
|
2020-10-10 08:23:49 -07:00 |
|
Leonardo de Moura
|
b0564a32b9
|
feat: add AttrM
We are going to use `AttrM` to implement solution 2 described at https://github.com/leanprover/lean4/issues/175
|
2020-09-21 16:44:20 -07:00 |
|
Leonardo de Moura
|
d33f7c7885
|
feat: attribute command
|
2020-09-20 09:11:36 -07:00 |
|
Leonardo de Moura
|
d5cb3aa85a
|
chore: add elabAttr
WIP
|
2020-09-20 07:51:11 -07:00 |
|
Leonardo de Moura
|
11e65fba2a
|
refactor: factor out macros from mutual elaborator
|
2020-09-19 13:10:10 -07:00 |
|
Leonardo de Moura
|
d0993d07a1
|
chore: rename Definition.lean => DefView.lean
|
2020-09-06 08:40:48 -07:00 |
|
Leonardo de Moura
|
d8855c2673
|
feat: elaborate all definitions using elabMutualDef
|
2020-09-06 07:23:47 -07:00 |
|
Leonardo de Moura
|
f5fea33651
|
chore: mark TODOs
|
2020-09-01 17:07:01 -07:00 |
|
Leonardo de Moura
|
5ced8867b0
|
feat: anonymous instances and support for all kinds of definition at mutual
|
2020-09-01 17:00:00 -07:00 |
|
Leonardo de Moura
|
d74551b19e
|
feat: elaborate header of mutually recursive definitions
|
2020-09-01 16:13:04 -07:00 |
|
Leonardo de Moura
|
356b11578b
|
chore: add helper functions
|
2020-09-01 16:11:27 -07:00 |
|
Leonardo de Moura
|
dfd344c9eb
|
chore: add MutualDef.lean
|
2020-09-01 14:18:10 -07:00 |
|
Leonardo de Moura
|
b9d50d2adf
|
refactor: expandDeclId
|
2020-09-01 13:12:36 -07:00 |
|
Leonardo de Moura
|
5e5b75af61
|
chore: remove withDeclId
|
2020-09-01 13:04:08 -07:00 |
|
Leonardo de Moura
|
d7e99c76c3
|
feat: mutual + namespace macro
|
2020-09-01 12:25:29 -07:00 |
|
Leonardo de Moura
|
5da3d9bf70
|
fix: quotation
|
2020-08-31 16:35:37 -07:00 |
|
Leonardo de Moura
|
8e179ed829
|
feat: macros in mutual blocks and elabMutualDef entry point
|
2020-08-31 15:37:41 -07:00 |
|
Leonardo de Moura
|
6f1975aef5
|
feat: report errors for unassigned metavariables
We were not reporting unassigned metavariables due to
1- `_`
2- Named holes (e.g., `?x`)
3- Implicit arguments
|
2020-08-27 15:03:41 -07:00 |
|
Leonardo de Moura
|
bb3c8a2105
|
refactor: polymorphic applyAttributes
|
2020-08-27 10:46:33 -07:00 |
|
Leonardo de Moura
|
813a964767
|
refactor: move polymorphic Meta methods back to Meta namespace
|
2020-08-25 14:57:58 -07:00 |
|
Leonardo de Moura
|
ac565de96c
|
refactor: add MonadMetaM class
|
2020-08-24 12:17:47 -07:00 |
|
Leonardo de Moura
|
5ffbada3df
|
feat: add Lean.MonadEnv, Lean.MonadError, and Lean.MonadOptions
This is the first set of polymorphic methods. I will add more later,
and keep reducing code duplication.
cc @Kha
|
2020-08-22 16:00:43 -07:00 |
|
Leonardo de Moura
|
5ba9aad7a3
|
refactor: eliminate ref plumbing
|
2020-08-13 10:37:53 -07:00 |
|
Leonardo de Moura
|
bd7a7ed623
|
refactor: reduce ref plumbing
TODO: reduce `ref` plumbing at `CommandElabM`
|
2020-08-12 20:23:02 -07:00 |
|
Leonardo de Moura
|
795b5d600a
|
feat: add expandFields
|
2020-07-17 11:10:34 -07:00 |
|
Leonardo de Moura
|
d2f26e142d
|
chore: naming
|
2020-07-17 09:18:20 -07:00 |
|