Leonardo de Moura
203bf08339
refactor: try ==> commitWhen
2020-02-14 19:17:11 -08:00
Leonardo de Moura
ddf6ecaea3
chore: remove dead code
2020-02-14 19:11:15 -08:00
Leonardo de Moura
551f6ebcd0
feat: rewriteCore tactic
2020-02-14 09:40:29 -08:00
Leonardo de Moura
c30c14ec84
chore: update stage0
2020-02-13 18:27:58 -08:00
Leonardo de Moura
0cf226220c
fix: remove incorrect assertion
...
Note that `get_cases_on_minors_range` is now parametric on `m_before_erasure`:
`get_cases_on_minors_range(env(), const_name(fn), m_before_erasure)`
2020-02-13 18:26:12 -08:00
Leonardo de Moura
47aba91c43
feat: error message when optParam and autoParam are used at fun
2020-02-13 17:57:12 -08:00
Leonardo de Moura
2fa19b5881
chore: cleanup
2020-02-13 16:39:36 -08:00
Leonardo de Moura
da3bf54ec7
feat: elaborate autoParams
...
cc @Kha
2020-02-13 16:24:50 -08:00
Leonardo de Moura
fd7727cf81
feat: helper functions for updating SourceInfo
2020-02-13 16:22:28 -08:00
Leonardo de Moura
44817b8488
feat: autoParam takes the Name of an auxiliary declaration of type Syntax
...
@Kha The `Name` (tactic name) approach used in Lean3 is not suitable
for Lean4. The issue is that we define tactics using macros, and in
most cases, the user doesn't even know the node id.
2020-02-13 15:09:42 -08:00
Leonardo de Moura
2507ce206e
feat: change auto param syntax
2020-02-13 11:56:24 -08:00
Leonardo de Moura
93de4ce7b3
feat: elaborate by
2020-02-13 11:45:51 -08:00
Leonardo de Moura
8778b68a5a
chore: update stage0
2020-02-13 11:38:58 -08:00
Leonardo de Moura
f041dd1aa1
feat: add by notation
2020-02-13 11:34:24 -08:00
Leonardo de Moura
cc2f84aa5d
fix: allow empty sequence at seq
2020-02-13 11:34:09 -08:00
Leonardo de Moura
4fe0104b52
feat: add autoParam
2020-02-13 10:53:01 -08:00
Leonardo de Moura
d62aafdb94
doc: @ cases that are supported
2020-02-13 10:29:29 -08:00
Leonardo de Moura
03a87df618
doc: elabFunBinders support for implicit lambdas
...
cc @Kha
2020-02-13 10:16:48 -08:00
Leonardo de Moura
4227d3bce4
chore: reduce problem size
...
Motivation: avoid stack overflow in debug mode
2020-02-12 21:27:34 -08:00
Leonardo de Moura
8094d35366
chore: update stage0
2020-02-12 17:20:46 -08:00
Leonardo de Moura
263d22576b
test: add new implicit lambda test
2020-02-12 13:47:54 -08:00
Leonardo de Moura
1fe92ade36
doc: document why example fails
2020-02-12 13:46:55 -08:00
Leonardo de Moura
6c16deded4
feat: improve implicit lambdas
2020-02-12 13:38:01 -08:00
Leonardo de Moura
f85678cc25
feat: improve failIfSucceeds
2020-02-12 13:33:40 -08:00
Leonardo de Moura
fc404af645
feat: solve ?m t =?= c even when constApprox is disabled
2020-02-12 13:21:56 -08:00
Leonardo de Moura
be730fa27f
feat: add #check_failure as keyword
2020-02-12 12:52:51 -08:00
Leonardo de Moura
e35f79feb5
feat: postpone only if inferred type is unknown and there are arguments
2020-02-12 12:26:24 -08:00
Leonardo de Moura
7cd0e0a7a5
feat: make sure we can see error messages at #check_failure
2020-02-12 12:23:43 -08:00
Leonardo de Moura
98c925ed7e
feat: elaborate #check_failure
2020-02-12 11:55:02 -08:00
Leonardo de Moura
783460af4b
chore: update stage0
2020-02-12 11:30:15 -08:00
Leonardo de Moura
d15f3431dc
feat: add #check_failure command
2020-02-12 11:28:44 -08:00
Leonardo de Moura
9221a9d349
fix: typo at consumeLet
2020-02-12 10:17:30 -08:00
Leonardo de Moura
6429486f88
refactor: decouple elaboration for forall and lambda binders
...
Motivation: another refactoring to improve `elabFunCore`.
2020-02-12 09:11:20 -08:00
Leonardo de Moura
fae52a7ba6
fix: @($f:fun) case
2020-02-12 08:46:25 -08:00
Leonardo de Moura
17dfe3fb66
test: implicit lambda tests
2020-02-11 21:21:21 -08:00
Leonardo de Moura
f0e3cf449f
fix: unhygienic method
2020-02-11 21:15:05 -08:00
Leonardo de Moura
61e57318eb
fix: assigning a delayed assigned metavar
2020-02-11 21:03:24 -08:00
Leonardo de Moura
41baf46083
feat: propagate expected type at elabFunCore
2020-02-11 17:47:51 -08:00
Leonardo de Moura
abd0f54ce6
chore: minor reorg before improving elabFunCore
2020-02-11 17:20:20 -08:00
Leonardo de Moura
97dfe95b41
chore: fix test
...
and document why better expected type propagation broke this example.
2020-02-11 16:26:39 -08:00
Leonardo de Moura
5e400dfe57
feat: use isTypeFormer
2020-02-11 16:13:41 -08:00
Leonardo de Moura
2f959e23ca
fix: checkAssignment was overwriting assignment
2020-02-11 16:11:56 -08:00
Leonardo de Moura
55231b960e
feat: simplify and improve processAssignmentFOApproxAux
2020-02-11 14:42:02 -08:00
Leonardo de Moura
30e0ccd8c4
feat: implicit lambdas
...
It is still work in progress
2020-02-11 13:43:05 -08:00
Leonardo de Moura
8044682b34
fix: type class instance arguments _ at explicit applications @f _ _
2020-02-11 13:36:52 -08:00
Leonardo de Moura
03b5b7d562
feat: implicit lambdas
2020-02-11 09:59:46 -08:00
Leonardo de Moura
4f91e0b0d9
feat: propagate before final ensureHasType
2020-02-11 09:59:23 -08:00
Leonardo de Moura
ae8eab42ca
feat: update @ elaborator
2020-02-11 09:35:37 -08:00
Leonardo de Moura
adb940e879
feat: new test
2020-02-11 09:34:45 -08:00
Leonardo de Moura
f4c1c5b0a6
chore: update stage0
2020-02-11 09:08:11 -08:00
