Leonardo de Moura
|
7cfd3f13ca
|
chore: update function name
|
2020-01-17 17:48:18 -08:00 |
|
Leonardo de Moura
|
ea45c6a9c5
|
chore: update stage0
|
2020-01-17 17:44:25 -08:00 |
|
Leonardo de Moura
|
d16a979931
|
chore: remove auxiliary code and parser for _app_
|
2020-01-17 17:43:44 -08:00 |
|
Leonardo de Moura
|
53c75e201a
|
chore: update stage0
|
2020-01-17 17:40:43 -08:00 |
|
Leonardo de Moura
|
47fb604e78
|
chore: remove auxiliary _app_
|
2020-01-17 17:39:44 -08:00 |
|
Leonardo de Moura
|
eda70a5567
|
chore: update stage0
|
2020-01-17 17:36:17 -08:00 |
|
Leonardo de Moura
|
0caa11e242
|
chore: adjust frontend to new app representation, and fix tests
|
2020-01-17 17:34:48 -08:00 |
|
Leonardo de Moura
|
ee0118bd2f
|
chore: update stage0
|
2020-01-17 16:49:57 -08:00 |
|
Leonardo de Moura
|
e4123585b2
|
feat: modify app representation
|
2020-01-17 16:49:22 -08:00 |
|
Leonardo de Moura
|
749b6b1b7e
|
chore: update stage0
|
2020-01-17 16:16:29 -08:00 |
|
Leonardo de Moura
|
1a217db3e9
|
chore: use auxiliary _app_ at Quotation
|
2020-01-17 16:15:49 -08:00 |
|
Leonardo de Moura
|
2eafb70585
|
chore: add auxiliary functions and simplify Quotation
|
2020-01-17 16:00:39 -08:00 |
|
Leonardo de Moura
|
d9dfaae3b8
|
feat: elaborate auxiliary app notation
|
2020-01-17 15:49:00 -08:00 |
|
Leonardo de Moura
|
a7025da89d
|
chore: add auxiliary app notation
|
2020-01-17 15:48:42 -08:00 |
|
Leonardo de Moura
|
395b0aed02
|
chore: update stage0
|
2020-01-17 09:46:43 -08:00 |
|
Sebastian Ullrich
|
ec8227cfd4
|
fix: antiquotation kinds :term should not be new tokens
|
2020-01-17 09:42:34 -08:00 |
|
Leonardo de Moura
|
f2231ebbc0
|
feat: improve macro command parser
|
2020-01-17 09:37:36 -08:00 |
|
Leonardo de Moura
|
611796851f
|
chore: update stage0
|
2020-01-17 08:12:20 -08:00 |
|
Leonardo de Moura
|
36d508a4ce
|
feat: simplify macroArg
|
2020-01-17 08:11:19 -08:00 |
|
Leonardo de Moura
|
a98b6763ad
|
fix: code and tests
|
2020-01-17 08:11:06 -08:00 |
|
Leonardo de Moura
|
b325db6ca0
|
chore: update stage0
|
2020-01-17 07:45:47 -08:00 |
|
Leonardo de Moura
|
257b5e27f3
|
feat: stx modifications
|
2020-01-17 07:44:51 -08:00 |
|
Leonardo de Moura
|
afefe93cc2
|
chore: update stage0
|
2020-01-16 20:58:07 -08:00 |
|
Leonardo de Moura
|
14ae1166b1
|
feat: add unboxSingleton trick to sepBy1
|
2020-01-16 20:57:18 -08:00 |
|
Leonardo de Moura
|
96253f3f2a
|
chore: update stage0
|
2020-01-16 20:26:08 -08:00 |
|
Leonardo de Moura
|
ccd7af0008
|
feat: display unsolved goals
|
2020-01-16 20:25:22 -08:00 |
|
Leonardo de Moura
|
8862a82aac
|
feat: add MessageData.ofGoal
|
2020-01-16 20:22:38 -08:00 |
|
Leonardo de Moura
|
833b1b0ff3
|
feat: add evalIntro
|
2020-01-16 20:10:24 -08:00 |
|
Leonardo de Moura
|
8f59d4a9e6
|
fix: assignDelayed misuse at intro
|
2020-01-16 20:09:27 -08:00 |
|
Leonardo de Moura
|
5a1221c491
|
chore: add helper
|
2020-01-16 19:54:00 -08:00 |
|
Leonardo de Moura
|
41a093f2df
|
feat: also return true if term contain delayed assignments
|
2020-01-16 19:53:11 -08:00 |
|
Leonardo de Moura
|
f6622b3120
|
fix: display goal at error
|
2020-01-16 19:32:58 -08:00 |
|
Leonardo de Moura
|
72c6194d9b
|
fix: typos
|
2020-01-16 19:28:49 -08:00 |
|
Leonardo de Moura
|
dc2c664ad1
|
feat: display goal when tactic fails
|
2020-01-16 19:23:02 -08:00 |
|
Leonardo de Moura
|
c25f9ad014
|
feat: add ppGoal
|
2020-01-16 19:16:06 -08:00 |
|
Leonardo de Moura
|
766c173746
|
feat: add ppExprFn extension
It hides `ppOld`, and allows users to change the pretty printer.
|
2020-01-16 18:31:02 -08:00 |
|
Leonardo de Moura
|
e654909f7a
|
feat: add Exception.tactic
|
2020-01-16 18:21:11 -08:00 |
|
Leonardo de Moura
|
57ebfa45d2
|
chore: update stage0
|
2020-01-16 17:53:30 -08:00 |
|
Leonardo de Moura
|
a6c745e93e
|
feat: allow underscore to be used as identifier
|
2020-01-16 17:51:01 -08:00 |
|
Leonardo de Moura
|
6077ac562f
|
chore: update stage0
|
2020-01-16 17:34:10 -08:00 |
|
Leonardo de Moura
|
c32e9abd8f
|
feat: add `(tactic| ...) notation
@kha please check
|
2020-01-16 17:32:47 -08:00 |
|
Leonardo de Moura
|
c7d96a6522
|
fix: theorem values are tasks
|
2020-01-16 17:20:36 -08:00 |
|
Leonardo de Moura
|
293990a309
|
feat: add eval for seq and assumption
|
2020-01-16 17:04:21 -08:00 |
|
Leonardo de Moura
|
0156a41699
|
chore: update stage0
|
2020-01-16 16:54:05 -08:00 |
|
Leonardo de Moura
|
1f673f1624
|
refactor: improve names, fields, etc
|
2020-01-16 16:53:07 -08:00 |
|
Leonardo de Moura
|
0b26fd2983
|
feat: allow empty begin .. end blocks, better position information
|
2020-01-16 16:07:59 -08:00 |
|
Leonardo de Moura
|
8e78fb177a
|
feat: basic runTactic
|
2020-01-16 16:01:53 -08:00 |
|
Leonardo de Moura
|
0c9107fc72
|
feat: add instantiateLCtxMVars and instantiateMVarDeclMVars
|
2020-01-16 15:45:40 -08:00 |
|
Leonardo de Moura
|
b0298697c5
|
feat: add runTactic skelethon
|
2020-01-16 14:58:23 -08:00 |
|
Leonardo de Moura
|
49636c531f
|
feat: add SynthesizeSyntheticMVars.lean
Reason: it depends on to include `Tactic.lean`, and `Tactic.lean`
depends on `Term.lean`
|
2020-01-16 12:58:37 -08:00 |
|