Leonardo de Moura
80e00a87c6
feat: add declare_syntax_cat command parser
2020-01-10 20:38:08 -08:00
Leonardo de Moura
799914daf2
feat: registerParserCategory
2020-01-10 20:32:16 -08:00
Leonardo de Moura
3c8d8c7434
feat: add attributeExtension
2020-01-10 19:51:53 -08:00
Leonardo de Moura
48600dbbfc
refactor: registerAttribute ==> registerBuiltinAttribute
2020-01-10 17:08:12 -08:00
Leonardo de Moura
6fc158f550
chore: update stage0
2020-01-10 15:22:16 -08:00
Leonardo de Moura
f783115d21
refactor: SyntaxNode => Syntax at TermElab and CommandElab
...
@Kha It is too annoying to write `.val` all over the place. Moreover,
we now have `match_syntax`.
2020-01-10 15:17:58 -08:00
Leonardo de Moura
f73ff914eb
feat: extensible elaboration functions
...
@kha `termParserAttr.lean` has a small example
2020-01-10 15:05:14 -08:00
Leonardo de Moura
f60c8c6249
test: add kabstract tests
2020-01-10 13:30:50 -08:00
Leonardo de Moura
63cd3a8c41
fix: nontermination at isDefEqOffset
2020-01-10 13:25:20 -08:00
Leonardo de Moura
06b6beb9f7
feat: add kabstract
2020-01-10 13:10:03 -08:00
Leonardo de Moura
3077d13b56
feat: add HeadIndex
2020-01-10 11:58:22 -08:00
Leonardo de Moura
947438afbe
feat: add Occurrences
2020-01-10 11:06:36 -08:00
Leonardo de Moura
a76b104f61
chore: move Message to Lean
2020-01-10 10:58:50 -08:00
Leonardo de Moura
f8c7d6ca6b
feat: elaborate optParam
2020-01-10 09:32:01 -08:00
Leonardo de Moura
d7b23cf297
fix: typo
2020-01-10 08:36:48 -08:00
Daniel Selsam
27158eb3e2
fix: DiscrTree typos
2020-01-10 08:07:41 -08:00
Leonardo de Moura
c5111de0f0
feat: add option set_option synthInstance.maxSteps <num>
...
cc @dselsam @kha
2020-01-10 08:04:25 -08:00
Leonardo de Moura
733ea89000
feat: improve application type mismatch error message
2020-01-09 16:41:27 -08:00
Leonardo de Moura
693d7dcf62
test: add class projection test
2020-01-09 16:25:12 -08:00
Leonardo de Moura
a4c2b0303e
chore: update stage0
2020-01-09 16:12:42 -08:00
Leonardo de Moura
e2ad834a2c
fix: weird bug that only occurs in debug mode
2020-01-09 16:11:33 -08:00
Leonardo de Moura
c45218be1a
chore: update-stage0
2020-01-09 15:43:46 -08:00
Leonardo de Moura
56d6961529
fix: old constant names
2020-01-09 15:40:55 -08:00
Leonardo de Moura
de24a3b205
chore: update stage0
2020-01-09 15:40:18 -08:00
Leonardo de Moura
bba9cdd8ff
feat: improve support for nat literals
2020-01-09 15:36:46 -08:00
Leonardo de Moura
654b464747
chore: improve old pretty printer on numeric literals
2020-01-09 13:48:15 -08:00
Leonardo de Moura
3d1ee3f408
fix: add isNewAnswer predicate
...
reactivate `typeclass_coerce.lean` test
2020-01-09 13:37:21 -08:00
Leonardo de Moura
125faad936
fix: missing do
...
This is nasty. The following
```
if entry.answers.contains answer then pure () -- if answer was already found, then do nothing
else
let newEntry := { answers := entry.answers.push answer, .. entry };
modify $ fun s => { tableEntries := s.tableEntries.insert key newEntry, .. s };
entry.waiters.forM (wakeUp answer)
```
was being parsed as
```
if entry.answers.contains answer then pure () -- if answer was already found, then do nothing
else
(let newEntry := { answers := entry.answers.push answer, .. entry };
modify $ fun s => { tableEntries := s.tableEntries.insert key newEntry, .. s });
entry.waiters.forM (wakeUp answer)
```
2020-01-09 12:44:41 -08:00
Leonardo de Moura
c49e43f69f
chore: reactivate typeclass test
2020-01-09 11:47:48 -08:00
Leonardo de Moura
bc393a750d
chore: reactivate typeclass test
...
I had to split the test because `new_frontend` command consumes the
rest of the file.
2020-01-09 11:46:10 -08:00
Leonardo de Moura
178e411031
chore: reactivate typeclass_append
2020-01-09 11:40:34 -08:00
Leonardo de Moura
f3d4005fc6
fix: outParam support
2020-01-09 11:39:12 -08:00
Leonardo de Moura
78c50125dd
fix: bug preprocessArgs
2020-01-09 11:13:25 -08:00
Leonardo de Moura
21e2d3b80f
chore: reactivate typeclass_diamond.lean
2020-01-09 10:49:01 -08:00
Leonardo de Moura
ebd20432b6
fix: isDefEqOffset
2020-01-09 10:47:02 -08:00
Leonardo de Moura
11d15575f7
feat: ignore Nat.succ, Nat.zero Nat.add and HasAdd.add at `DiscrTree
...
@dselsam We need this feature to be able to retrieve instances of the
form `Top (Nat.succ ?m)` given `Top 1` where `1` is the literal `1`
2020-01-09 10:28:09 -08:00
Leonardo de Moura
f49e1cd0fb
fix: isDefEqOffset
2020-01-09 10:10:32 -08:00
Leonardo de Moura
2a8e179a64
feat: add #synth command to new frontend
2020-01-09 09:54:45 -08:00
Leonardo de Moura
923bd321ef
chore: remove unnecessary commands
2020-01-09 09:45:07 -08:00
Leonardo de Moura
984257af29
chore: update stage0
2020-01-09 09:44:07 -08:00
Leonardo de Moura
5888a790d1
feat: add #synth command to new frontend
2020-01-09 09:42:22 -08:00
Leonardo de Moura
1b7d9cc6e5
chore: update stage0
2020-01-08 21:24:33 -08:00
Leonardo de Moura
65370e9322
chore: restore disabled tests
2020-01-08 21:24:01 -08:00
Leonardo de Moura
c06d515027
fix: typo
2020-01-08 21:22:46 -08:00
Leonardo de Moura
48578c9743
chore: remove hacks
2020-01-08 21:09:17 -08:00
Leonardo de Moura
74b504ad05
chore: update stage0
2020-01-08 21:09:17 -08:00
Leonardo de Moura
981e35b6da
chore: style
2020-01-08 21:09:17 -08:00
Leonardo de Moura
760f8aa013
chore: fix tests
2020-01-08 21:09:17 -08:00
Leonardo de Moura
d818fc90ce
chore: update stage0
2020-01-08 21:09:17 -08:00
Leonardo de Moura
4550e75dcb
chore: temporary hack for solving staging issue
2020-01-08 21:09:17 -08:00
