Leonardo de Moura
238f96b616
feat: add StateCpsT
2021-02-27 18:21:19 -08:00
Leonardo de Moura
6a6f68f6cc
feat: missing lemmas
2021-02-27 10:42:30 -08:00
Leonardo de Moura
b9ef6f89a4
chore: cleanup
2021-02-26 19:34:39 -08:00
Leonardo de Moura
5662e2e745
refactor: move ToString Syntax and BEq Syntax to Init
2021-02-26 13:21:04 -08:00
Sebastian Ullrich
8b20a939aa
fix: Reader
2021-02-26 14:58:09 +01:00
Leonardo de Moura
d3a914c1ff
chore: cleanup
2021-02-23 12:52:14 -08:00
Leonardo de Moura
162062b3de
feat: improve Lawful.lean
2021-02-23 12:38:00 -08:00
Leonardo de Moura
98348dfe7f
feat: add ExceptT.run_bind_lift and ExceptT.bind_throw
...
Remove `[simp]` attribute from `ExceptT.run_bind`
2021-02-23 08:17:11 -08:00
Leonardo de Moura
d0574d8eb1
feat: add LawfulMonad for StateT
2021-02-21 10:52:53 -08:00
Leonardo de Moura
b1faed895a
chore: change inferInstance and inferInstanceAs types
2021-02-21 08:36:03 -08:00
Leonardo de Moura
ae48feeb07
feat: add LawfulMonad for ReaderT
2021-02-21 08:27:59 -08:00
Leonardo de Moura
d77f335ff0
feat: add LawfulMonad instance for ExceptT
2021-02-20 17:01:27 -08:00
Leonardo de Moura
caf54d78e2
feat: add Control/Lawful.lean
2021-02-20 09:37:43 -08:00
Leonardo de Moura
e1f6965266
feat: allow user to define rewrite lemmas with (local) match expressions
2021-02-19 15:18:19 -08:00
Leonardo de Moura
79a4aebf96
feat: add byCases tactic
2021-02-17 13:03:24 -08:00
Sebastian Ullrich
187a614575
chore: make tryFinally a def
2021-02-17 12:04:20 +01:00
Leonardo de Moura
d1009e8405
chore: add simp lemmas, theorem naming convention
2021-02-16 11:53:49 -08:00
Leonardo de Moura
504a015f9b
fix: borrowing annotations
2021-02-16 10:30:30 -08:00
Sebastian Ullrich
e8812ed834
fix: memory leak at Nat.ble
2021-02-16 14:24:28 +01:00
Leonardo de Moura
4ec85a39a5
fix: Not should not be reducible, special support for Ne
...
Unification hint for `Not`
2021-02-15 17:36:11 -08:00
Leonardo de Moura
99ba21a881
chore: annotations for simp
2021-02-15 17:04:47 -08:00
Leonardo de Moura
1c5de9842d
feat: use decide at simp
2021-02-15 13:08:45 -08:00
Leonardo de Moura
51bdf670fa
chore: add simp helper lemmas
2021-02-15 12:42:13 -08:00
Leonardo de Moura
9528c1abd7
chore: add basic simp lemmas
...
TODO: consistent naming convention for theorems.
cc @Kha
2021-02-15 11:32:19 -08:00
Leonardo de Moura
2944da2a0b
feat: use simp itself as default method for discharging hypotheses of conditional rewriting rules
2021-02-13 18:55:19 -08:00
Leonardo de Moura
1a4eaa2418
chore: arguments occurring in the lhs should be marked as implicit
2021-02-13 18:55:19 -08:00
Sebastian Ullrich
75243e7f24
feat: change back seqLeft/Right signature
...
This was originally changed for the sake of `do`, which does not depend on it anymore
2021-02-12 17:08:06 -08:00
Leonardo de Moura
16a6778fb6
fix: avoid nonstandard instances at ite and dite congruence lemmas
...
cc @gebner
2021-02-12 16:52:56 -08:00
Leonardo de Moura
3a66dbf0fd
chore: annotate ite/dite congruence lemmas
2021-02-11 17:55:42 -08:00
Leonardo de Moura
c0f5ab1fa5
feat: add congruence lemmas for simp
2021-02-11 14:07:01 -08:00
Leonardo de Moura
09ad6cc50a
fix: fixes #306 fixes #307
2021-02-06 12:31:51 -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
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
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
d956f0ae9f
feat: use destructTuple to compile for in notation instead of pattern matchin
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
f4c9f7e163
chore: remove id_delta (aka idDelta)
...
It is a leftover from Lean 3.
2021-02-02 13:59:37 -08:00
Leonardo de Moura
fba719ff02
chore: adjust WF.lean
2021-02-01 18:08:48 -08:00
Leonardo de Moura
e583b3bdc0
feat: allow @ modifier at inductionAlt
2021-02-01 17:13:51 -08:00
Leonardo de Moura
af7db05000
chore: remove nested outParam
2021-01-29 17:13:03 -08:00
Wojciech Nawrocki
28d6a1ebe1
fix: go-to-def paths on Windows
2021-01-28 11:45:33 -08:00
Leonardo de Moura
4a19a5d2a4
refactor: move Eq.trans to Prelude.lean
...
We need it at `SizeOf.lean`
2021-01-27 18:27:04 -08:00
Leonardo de Moura
5f704b6b6f
chore: fix option name
2021-01-26 18:30:46 -08:00
Leonardo de Moura
be7ddef689
refactor: move congr and congrFun to Prelude.lean
...
We use them to generate the `sizeOf` lemmas.
2021-01-25 17:18:08 -08:00
Leonardo de Moura
d408c835d2
fix: defaultInstance priorities for Neg Int and OfScientific Float
2021-01-25 13:21:07 -08:00
Leonardo de Moura
d834d88b88
fix: performance bottleneck
...
@Kha @dselsam
The instances
```
instance (sep) : Coe (Array Syntax) (SepArray sep)
instance (sep) : Coe (SepArray sep) (Array Syntax)
```
The instances above generate a loop. The current `isNewAnswer`
predicate is too weak and assumes that answers with different
metavariables are different. Note that, using `isDefEq` there is
incorrect and too expensive. I will fix this later in the future.
In the meantime, I am using `CoeTail` to avoid the loop.
2021-01-24 17:45:50 -08:00
Leonardo de Moura
7ff62ee46b
feat: add CoeHTCT
2021-01-24 17:45:50 -08:00
Leonardo de Moura
acfac85ac0
feat: add IO.getNumHeartbeats
2021-01-24 17:45:50 -08:00
