Scott Morrison
|
bf6d9295a4
|
chore: shaking imports in Init.Data.Nat/Int (#3605)
|
2024-03-05 13:29:35 +00:00 |
|
Scott Morrison
|
6048ba9832
|
chore: upstream Std.Classes.LawfulMonad (except SatisfiesM) (#3340)
|
2024-02-15 01:52:02 +00:00 |
|
ChrisHughes24
|
e168806078
|
chore: rename Prod.ext
|
2022-12-02 20:24:19 +01:00 |
|
Mario Carneiro
|
d875f43b52
|
chore: remove outdated TODO
|
2022-08-26 15:31:13 -07:00 |
|
Mario Carneiro
|
6906a4d1ee
|
feat: generalize ReaderT definitions
|
2022-08-12 08:23:11 -07:00 |
|
Mario Carneiro
|
f6211b1a74
|
chore: convert doc/mod comments from /- to /--//-! (#1354)
|
2022-07-22 12:05:31 -07:00 |
|
Leonardo de Moura
|
46b97c2b70
|
fix: ExceptT.run_lift
|
2022-02-28 07:25:00 -08:00 |
|
Leonardo de Moura
|
82e3789604
|
fix: run_lift type
|
2022-02-25 07:49:34 -08:00 |
|
Leonardo de Moura
|
3ccd44fafa
|
fix: proofs after adding eta struct support at recursors
see #777
|
2021-11-25 11:34:31 -08:00 |
|
Leonardo de Moura
|
e15a656fd2
|
fix: remove @[reducible] annotation from Function.comp and Function.const
closes #813
|
2021-11-23 07:29:25 -08:00 |
|
Leonardo de Moura
|
9fde1d53b7
|
chore: adjust proofs affected by struct eta
closes #777
|
2021-11-23 06:23:50 -08:00 |
|
Leonardo de Moura
|
2c037c3989
|
chore: fix proofs
|
2021-07-29 16:59:47 -07:00 |
|
Leonardo de Moura
|
3b5e762882
|
chore: add temporary workaround
|
2021-07-27 14:23:05 -07:00 |
|
Sebastian Ullrich
|
a02c6fd3eb
|
chore: adapt stdlib & tests
|
2021-05-20 15:17:36 -07:00 |
|
Leonardo de Moura
|
3d58c4d115
|
chore: remove old notation
|
2021-03-12 15:05:06 -08:00 |
|
Leonardo de Moura
|
904c23e901
|
chore: add annotations
We need these extra annotations after we fix a bug a `commitWhen`.
In the `commitWhen` bug, we were "losing" postponed constraints.
|
2021-03-10 14:11:03 -08:00 |
|
Leonardo de Moura
|
6a6f68f6cc
|
feat: missing lemmas
|
2021-02-27 10:42:30 -08: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
|
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 |
|