Leonardo de Moura
21353d07d5
fix: unassigned universe metavariables should not block instantiation of delayed assignment
2020-03-08 17:31:07 -07:00
Leonardo de Moura
3b84507888
fix: expand show and have using let!
...
Motivation: expected elaboration order is preserved: first type, then
value, and then body.
Motivation: expected type is not lost when elaborating the body.
2020-03-08 16:14:11 -07:00
Leonardo de Moura
354bc450e6
feat: elaborate let!
2020-03-08 16:02:00 -07:00
Leonardo de Moura
d4d4e199bc
chore: remove dead code
2020-03-08 15:52:55 -07:00
Leonardo de Moura
de6fda9b37
feat: add let! notation
...
`let x := v; t` is elaborated into `(fun x => t) v`
2020-03-08 15:49:13 -07:00
Leonardo de Moura
783ca47d1f
fix: typo
2020-03-08 12:22:00 -07:00
Leonardo de Moura
502758b09c
fix: allow universe **level** metavariables
2020-03-08 11:33:35 -07:00
Leonardo de Moura
adce6df1a1
fead: add evalInjection
2020-03-08 11:31:43 -07:00
Leonardo de Moura
cbf7a661df
feat: add elabAsFVar
2020-03-08 11:31:18 -07:00
Leonardo de Moura
74908bb9c7
fix: typo
2020-03-08 11:31:05 -07:00
Leonardo de Moura
a708c5d134
feat: injection tactic notation
2020-03-08 10:34:39 -07:00
Leonardo de Moura
5ea1160e86
feat: add injection tactic
2020-03-08 10:34:31 -07:00
Leonardo de Moura
c493ac1e1e
feat: injectionCore tactic
2020-03-08 10:21:40 -07:00
Leonardo de Moura
5770edbffd
feat: workaround for the constant approximation issue
...
@Kha It seems to cover all the scenarios we discussed earlier today.
2020-03-06 16:47:02 -08:00
Leonardo de Moura
5ffde62343
fix: check runTactics
2020-03-06 15:39:53 -08:00
Leonardo de Moura
8db309a079
feat: remove hack
...
We can't solve
```
```
anymore, but the hack was unstable. For example, it is weird that the
one above could be solved, but the following failed.
```
```
The difference is that the types in the first example were atomic
`Unit` and `Bool`, but not in the second.
2020-03-06 13:43:19 -08:00
Leonardo de Moura
3c5d2d4269
refactor: cleanup
...
closes #112
Previous two commits contributed too.
2020-03-06 13:43:19 -08:00
Leonardo de Moura
bce4912505
fix: remove bad condition
...
Recall that `processAssignmentFOApprox` will unfold `v` if possible.
2020-03-06 13:43:19 -08:00
Leonardo de Moura
482e078b92
chore: minor cleanup
2020-03-06 13:43:19 -08:00
Leonardo de Moura
8b5d75a2dd
chore: missing space
2020-03-05 18:44:33 -08:00
Leonardo de Moura
35000ff4cd
feat: add mkNoConfusion
2020-03-05 18:44:33 -08:00
Leonardo de Moura
414f674bb6
feat: skip, subst and HEq => Eq transitions
2020-03-05 18:44:33 -08:00
Leonardo de Moura
d9fd9bb1b3
feat: add mkEqOfHEq
2020-03-05 18:44:33 -08:00
Leonardo de Moura
4eaee1147b
feat: unifyEqs skeleton
2020-03-05 18:44:33 -08:00
Leonardo de Moura
6fb526ee00
feat: add elimAuxIndices
2020-03-05 18:44:33 -08:00
Leonardo de Moura
8d7ed8a9b8
refactor: FVarSubst
2020-03-05 18:44:33 -08:00
Leonardo de Moura
2f60e82049
fix: isHeadBetaTarget
2020-03-05 18:44:33 -08:00
Leonardo de Moura
74c9d54362
feat: simple case
2020-03-05 18:44:33 -08:00
Leonardo de Moura
83383b505f
chore: auxiliary functions
2020-03-05 18:44:33 -08:00
Leonardo de Moura
b5ec4ef2bd
feat: add evalCases
2020-03-05 18:44:33 -08:00
Leonardo de Moura
9626ceda09
fix: eta expansion before lazy delta
2020-03-05 18:44:33 -08:00
Leonardo de Moura
4400c82c4d
feat: add cases tactic syntax
2020-03-04 19:00:37 -08:00
Leonardo de Moura
dfa392fa17
feat: add generalizeIndices
...
Helper tactic for `cases`
2020-03-04 16:27:01 -08:00
Leonardo de Moura
21ca370961
feat: add cases tactic skeleton
2020-03-02 17:55:56 -08:00
Leonardo de Moura
eca569f237
chore: use NonScalar
2020-03-02 17:55:33 -08:00
Leonardo de Moura
0893b62598
perf: avoid unnecessary overhead at HashSet
...
List instead of AssocList saves one word per entry.
2020-03-02 08:40:15 -08:00
Leonardo de Moura
641cf90cc9
feat: add StateM.subsingleton
2020-03-02 08:37:55 -08:00
Leonardo de Moura
58ddeedced
feat: add List.replace
2020-03-02 08:30:20 -08:00
Leonardo de Moura
88dc110260
feat: add Squash
2020-03-02 08:30:05 -08:00
Leonardo de Moura
b379bca28b
chore: rename PtrEqResult.yes ==> PtrEqResult.yesEqual
2020-03-02 08:29:49 -08:00
Leonardo de Moura
0f8b59eed7
fix: typo Prop => Type
2020-02-29 11:22:17 -08:00
Leonardo de Moura
684554e979
feat: add PtrEqResult
2020-02-29 11:00:50 -08:00
Leonardo de Moura
94cfcbbefe
chore: withPtrEqSubsingleton ==> withPtrEqResult
2020-02-29 10:12:06 -08:00
Leonardo de Moura
d511ddfa9e
feat: add SemiDeciable and withPtrEqSubsingleton
2020-02-29 09:50:31 -08:00
Leonardo de Moura
090b1e664d
feat: rename maxSharing => shareCommon
2020-02-28 10:53:41 -08:00
Leonardo de Moura
cca90b5f9f
chore: simplify withPtrEqDecEq
2020-02-27 11:45:02 -08:00
Leonardo de Moura
b83691baa2
feat: compute fvarSubst
2020-02-27 10:58:46 -08:00
Leonardo de Moura
2719eaeb63
fix: closes #119
2020-02-27 08:10:29 -08:00
Leonardo de Moura
53b57af125
fix: dangling file
2020-02-25 14:33:54 -08:00
Leonardo de Moura
cfd7fc8a87
fix: message::get_text
...
It was still using the old representation.
2020-02-25 14:20:55 -08:00
