Leonardo de Moura
9ba8a30fb2
feat: add Repr instance for CongrLemmas
2021-02-11 18:13:33 -08:00
Leonardo de Moura
3a66dbf0fd
chore: annotate ite/dite congruence lemmas
2021-02-11 17:55:42 -08:00
Leonardo de Moura
ffa4a577be
feat: add @[congr] attribute
2021-02-11 17:51:04 -08:00
Leonardo de Moura
8b3c61dbb0
fix: checkAssignment
2021-02-11 16:56:32 -08:00
Leonardo de Moura
5e0b6a404f
chore: naming convention
2021-02-11 15:05:26 -08:00
Leonardo de Moura
c0f5ab1fa5
feat: add congruence lemmas for simp
2021-02-11 14:07:01 -08:00
Sebastian Ullrich
8320ab6177
fix: syntax match: check identifiers (using strict equality)
2021-02-11 17:50:05 +01:00
Sebastian Ullrich
19306a844f
chore: delaborator: print BinderInfo.auxDecl as explicit
2021-02-11 12:13:22 +01:00
Sebastian Ullrich
10bcd0bc9e
fix: #check_failure
2021-02-11 11:30:37 +01:00
Sebastian Ullrich
a74960a4ab
fix: delaborator: match with shadowing
2021-02-11 11:30:25 +01:00
Leonardo de Moura
2aed9a4ec2
chore: special support for match d with | PUnit.unit => rhs
2021-02-10 09:54:12 -08:00
Leonardo de Moura
4e4194af41
feat: add autoBoundImplicit support for structure fields
2021-02-06 17:58:29 -08:00
Leonardo de Moura
023d7605fb
feat: add "transitivity" to "has_loose_bvars_in_domain"
2021-02-06 17:42:38 -08:00
Leonardo de Moura
09ad6cc50a
fix: fixes #306 fixes #307
2021-02-06 12:31:51 -08:00
Sebastian Ullrich
4d8859140c
feat: improve goal display markup
2021-02-06 17:25:26 +01:00
Sebastian Ullrich
1ca3176143
chore: TacticInfo.format: show range
2021-02-06 17:24:24 +01:00
Wojciech Nawrocki
ec903f58d2
feat: bare-bones goal request handler
2021-02-06 10:41:14 +01:00
Wojciech Nawrocki
2aa4a7957e
feat: configurable server edit delay
2021-02-06 10:41:14 +01:00
Wojciech Nawrocki
e383222f92
feat: hovers for fields & refactor
2021-02-06 10:41:14 +01:00
Leonardo de Moura
cb8c1368b4
chore: remove workaround
2021-02-05 18:11:31 -08:00
Leonardo de Moura
f51328ff11
feat: custom elaborator for forIn
...
This commit also moves `elabBinRel` to `Extra.lean`
2021-02-05 18:01:58 -08:00
Leonardo de Moura
2d6b59f4bb
feat: add dummy elabForIn
2021-02-05 17:02:57 -08:00
Leonardo de Moura
e3c3fc3165
feat: add helper macro forIn!
...
We are going to write a custom elaborator for `forIn` applications.
2021-02-05 16:51:06 -08:00
Leonardo de Moura
eb510c16c3
chore: remove two workarounds
...
They are not needed anymore after 83775b08cb
2021-02-05 15:21:57 -08:00
Leonardo de Moura
83775b08cb
fix: whnfCore not expanding delayed assignments
2021-02-05 15:14:12 -08:00
Leonardo de Moura
f57c184dbd
chore: remove = true old workarounds
...
@Kha The old `= true` workarounds are not needed anymore, they were
due to another issue and are not related to yesterday's issue.
That is, the one exposed by the `ForIn` typeclass.
2021-02-05 13:48:03 -08:00
Leonardo de Moura
4dc2a84302
fix: whnfCore
...
Update function before invoking `reduceMatcher?`
2021-02-05 13:40:39 -08:00
Leonardo de Moura
8c0346f00c
feat: improve binrel! macro
2021-02-05 13:28:57 -08:00
Leonardo de Moura
cab3c72374
fix: isDefEq for applications in WHNF
...
The issue fixed by this commit was exposed by c17a1c382f
2021-02-05 12:42:34 -08:00
Leonardo de Moura
09de37e8e5
chore: improve error message
2021-02-05 12:26:39 -08:00
Leonardo de Moura
c17a1c382f
fix: isDeltaCandidate?
...
It should return `some ...` only if `ConstantInfo` has a value.
2021-02-05 09:19:37 -08:00
Leonardo de Moura
10a10b38d8
fix: fixes #303
2021-02-05 07:53:18 -08:00
Leonardo de Moura
278d47c772
chore: add Repr instance for TransparencyMode
2021-02-04 20:40:05 -08:00
Leonardo de Moura
d0ffecd419
chore: consistency
...
Make sure `Array.all` and `Array.any` parameter order is similar to
`List.all` and `List.any`.
2021-02-04 20:39:28 -08:00
Leonardo de Moura
8a1433794b
chore: improve TC error message when there is a type mismatch
2021-02-04 19:20:39 -08:00
Leonardo de Moura
24d58b672c
chore: add temporary workarounds
2021-02-04 18:38:04 -08:00
Leonardo de Moura
3d4bc9f991
chore: provide ambient monad to forIn
2021-02-04 18:31:28 -08:00
Leonardo de Moura
53539b1dff
chore: use polymorphic method forIn
2021-02-04 18:13:01 -08:00
Leonardo de Moura
aae8a35150
feat: add ForIn type class
2021-02-04 17:59:44 -08:00
Leonardo de Moura
e415cfa632
chore: increase synthInstance.maxHeartbeats default
2021-02-04 17:36:12 -08:00
Leonardo de Moura
d956f0ae9f
feat: use destructTuple to compile for in notation instead of pattern matchin
2021-02-04 17:17:51 -08:00
Leonardo de Moura
c747230e28
refactor: move isMonad? to AppBuilder.lean
2021-02-04 17:17:51 -08:00
Leonardo de Moura
e2028e64ff
feat: add option maxUniverseOffset
...
Universe level offsets are supposed to be small numbers in practice.
2021-02-04 17:17:51 -08:00
Leonardo de Moura
d494756d00
fix: inline loop
2021-02-04 17:17:51 -08:00
Leonardo de Moura
768f2642bd
chore: document why alternative Stream design does not work
2021-02-04 17:17:51 -08:00
Sebastian Ullrich
bdf7b15a41
feat: basic unexpanders for Exists & Sigma
...
A bit brittle and not quite complete, but probably good enough in practice
2021-02-04 11:04:37 +01:00
Leonardo de Moura
dae0132439
fix: save/restore state at elabTypeWithAutoBoundImplicit
2021-02-03 15:04:18 -08:00
Leonardo de Moura
e63111b39a
fix: fixes #302
...
TODO: investigage error message duplication
2021-02-03 15:04:18 -08:00
Leonardo de Moura
1a15b0183b
chore: occursCheck semantics was confusing
2021-02-03 15:04:18 -08:00
Leonardo de Moura
d1efcab6f5
perf: improve occursCheck
2021-02-03 15:04:18 -08:00
