Sebastian Ullrich
fd4b9ffcf5
chore: update stage0
2020-01-06 10:09:26 -08:00
Sebastian Ullrich
bece6f7a32
feat: command quotations
2020-01-06 10:09:26 -08:00
Leonardo de Moura
ebd39de20d
feat: add collectFVars
2020-01-06 09:34:00 -08:00
Leonardo de Moura
573877dcdf
chore: cleanup
2020-01-06 09:33:11 -08:00
Leonardo de Moura
5be180910f
test: add applyAttributes test
2020-01-05 16:27:22 -08:00
Leonardo de Moura
af6f7f4bc8
chore: update stage0
2020-01-05 16:27:05 -08:00
Leonardo de Moura
0231841984
feat: applyAttributes
2020-01-05 16:22:46 -08:00
Leonardo de Moura
e344f46e66
chore: allow attributes to parse arguments
2020-01-05 15:58:58 -08:00
Leonardo de Moura
a24838dd7c
feat: add addDecl
2020-01-05 15:01:56 -08:00
Leonardo de Moura
26c386d756
chore: univNames ==> levelNames
2020-01-05 14:49:16 -08:00
Leonardo de Moura
7fd55477b2
feat: add sortDeclLevelParams
2020-01-05 14:35:14 -08:00
Leonardo de Moura
9134cef891
feat: add collectLevelParams
2020-01-05 13:47:08 -08:00
Leonardo de Moura
abc8811498
feat: add LevelSet and PersistentLevelSet
2020-01-05 13:26:25 -08:00
Leonardo de Moura
b0fd7ad264
feat: convert unassigned universe level mvars into parameters
2020-01-05 13:21:39 -08:00
Leonardo de Moura
c233225153
feat: add mkForallUsedOnly
...
This commit also fixes a bug at `mkBinding` for unused let-decls
2020-01-05 11:53:39 -08:00
Leonardo de Moura
647c7270bd
refactor: DefView
2020-01-05 09:43:36 -08:00
Leonardo de Moura
a3dba3a011
feat: add univMVarToParam
2020-01-05 09:07:01 -08:00
Leonardo de Moura
f827086f85
feat: elaborate definition type
2020-01-04 16:32:24 -08:00
Leonardo de Moura
93dbcc161a
refactor: break Declaration.lean into smaller files
2020-01-04 13:31:25 -08:00
Leonardo de Moura
6ca9a8c170
feat: better runTermElabM
2020-01-04 13:08:21 -08:00
Sebastian Ullrich
042f65fc69
feat: track macro scopes in CommandElab and synchronize them with TermElab
2020-01-04 09:41:45 -08:00
Leonardo de Moura
eb9d793e79
feat: def-like elaboration skeleton
2020-01-04 08:48:00 -08:00
Leonardo de Moura
52a27c08cf
chore: remove hack
2020-01-03 18:29:18 -08:00
Leonardo de Moura
bd2243d978
chore: update stage0
2020-01-03 18:25:01 -08:00
Leonardo de Moura
8628b52b21
feat: missing support for Empty.rec
2020-01-03 18:23:52 -08:00
Leonardo de Moura
2f3c6a8185
feat: check attribute name
2020-01-03 18:15:55 -08:00
Leonardo de Moura
bc7455e04e
refactor: CommandElabM and FrontendM in IO
2020-01-03 18:15:45 -08:00
Leonardo de Moura
3264210d88
chore: helper functions
2020-01-03 12:24:14 -08:00
Leonardo de Moura
2b4a7ae6a4
feat: elaborate declaration modifiers
2020-01-03 12:13:03 -08:00
Leonardo de Moura
54fd9a2e4a
chore: naming convention
2020-01-03 12:12:45 -08:00
Daniel Selsam
91f97fb0d9
fix: typos in SynthInstance.lean
2020-01-03 10:29:01 -08:00
Leonardo de Moura
e949a052ba
feat: elaborate where
2020-01-02 15:01:26 -08:00
Leonardo de Moura
6825938dec
chore: update stage0
2020-01-02 14:56:40 -08:00
Leonardo de Moura
3f51857275
feat: add where syntax
2020-01-02 14:55:18 -08:00
Leonardo de Moura
16aff9a182
feat: elaborate have
2020-01-02 14:16:20 -08:00
Leonardo de Moura
04a0907954
feat: add throwUnexpectedSyntax
...
@kha From now on, let's use `throwUnexpectedSyntax` instead of `unreachable!` at
`match_syntax`. The `unreachable!` makes sense when the syntax was
created by our parser, but ill-formed syntax may be created by macros,
and we have no control on how users will create the resulting syntax object.
2020-01-02 13:51:02 -08:00
Leonardo de Moura
9f69991d80
feat: elaborate show notation
2020-01-02 13:30:11 -08:00
Leonardo de Moura
a3675b99e6
feat: add parameter postponeOnError : Bool to synthesizeSyntheticMVarsStep
...
@Kha: I implemented the option 2 I described on Zulip.
2020-01-02 13:13:58 -08:00
Leonardo de Moura
db96b08257
feat: elaborate anonymous constructor
2020-01-02 10:41:04 -08:00
Leonardo de Moura
0ffd1526bd
feat: elaborate subtype
2020-01-02 10:12:19 -08:00
Daniel Selsam
b4e285f91a
fix: dead link in doc
2020-01-02 14:36:14 +01:00
Leonardo de Moura
8f805f5d2f
feat: elaborate if-then-else
2020-01-01 16:12:26 -08:00
Leonardo de Moura
cbe65a068e
fix: addLValArg
2020-01-01 16:02:55 -08:00
Leonardo de Moura
2ca96cb2b0
feat: include macroStack in error messages
2020-01-01 15:19:04 -08:00
Leonardo de Moura
b429794ebc
chore: naming convention
2020-01-01 15:04:20 -08:00
Leonardo de Moura
9d25a45074
feat: elaborate character literals
2020-01-01 14:37:40 -08:00
Leonardo de Moura
434c148800
test: add termElab attribute test
2020-01-01 14:16:49 -08:00
Sebastian Ullrich
2791cdf326
fix: interpreter::call_boxed: support under-application
...
/cc @leodemoura
2020-01-01 21:15:05 +01:00
Leonardo de Moura
d22abd85dd
test: minimal repro for evalConst crash
2020-01-01 11:02:38 -08:00
Leonardo de Moura
61403b556d
chore: update stage0
2020-01-01 11:00:56 -08:00
