Henrik Böving
741fac924a
chore: inline control primitives
2022-10-15 10:48:47 -07:00
Leonardo de Moura
1eda0fd734
chore: missing annotation
2022-10-14 20:38:06 -07:00
Leonardo de Moura
870de844dc
chore: annotate relevant monadic code with [alwaysInline]
...
TODO: after we delete old code generator, we should replace
`@[alwaysInline, inline]` with `@[alwaysInline]`.
Remainder: we want the old code generator to ignore `@[alwaysInline]`
annotations, in particular, the new ones on `instance` commands that
are actually annotations for the instance methods.
2022-10-12 19:48:02 -07:00
Mario Carneiro
97bcc7fd7c
feat: add ForM -> ForIn adapter
2022-09-25 06:40:56 -07:00
E.W.Ayers
993115a937
feat: Kleisli operators
2022-09-16 05:49:56 -07:00
Leonardo de Moura
0925051c51
chore: rename Reader to ReaderM
...
closes #1524
2022-08-26 20:59:17 -07: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
Ed Ayers
c3f58a7eab
feat: add a message if Lean 4 is called with the Lean 3 extension
2022-07-29 11:08:51 +00:00
Mario Carneiro
f6211b1a74
chore: convert doc/mod comments from /- to /--//-! ( #1354 )
2022-07-22 12:05:31 -07:00
Leonardo de Moura
02c4e548df
feat: replace constant with opaque
2022-06-14 17:02:59 -07:00
Leonardo de Moura
041827bed5
chore: unused variables
2022-06-07 17:54:10 -07:00
Leonardo de Moura
c2ddebc193
chore: unused variables
2022-06-07 16:47:04 -07:00
Sebastian Ullrich
ae7b895f7a
refactor: unname some unused variables
2022-06-07 16:37:45 -07:00
Leonardo de Moura
5aaccc8ebb
chore: remove OptionM
2022-05-04 15:30:10 -07:00
Leonardo de Moura
c65537aea5
feat: Option is a Monad again
...
TODO: remove `OptionM` after update stage0
see: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Do.20we.20still.20need.20OptionM.3F/near/279761084
2022-05-04 15:27:42 -07:00
Ed Ayers
d8e2d58da7
doc: InfoTree code review
...
Co-authored-by: Wojciech Nawrocki <wjnawrocki+gh@protonmail.com>
2022-04-15 09:07:35 -07:00
E.W.Ayers
9598e39c82
doc: InfoTree docstrings
2022-04-15 09:04:26 -07:00
E.W.Ayers
9fdb7429d4
doc: edits to MonadControl
2022-04-01 10:06:58 +02:00
E.W.Ayers
4c2fedae50
doc: fix @Kha's issues with MonadControl
2022-04-01 10:06:58 +02:00
E.W.Ayers
00151f39a1
doc: explain MonadControl
2022-03-29 15:55:08 -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
tydeu
8e79d88d29
feat: liftOption
2022-01-19 12:22:05 +01:00
Leonardo de Moura
bac91b9b5b
chore: remove arbitrary
2022-01-15 12:14:27 -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
Sebastian Ullrich
d8d7eba6c5
feat: liftExcept
2021-11-09 16:58:13 +01:00
Leonardo de Moura
35d9589401
feat: add MonadControl m (OptionT m)
2021-09-19 14:20:26 -07:00
Leonardo de Moura
3714cf16ec
refactor: lazy evaluation for <|>
...
see #617
2021-09-07 17:06:10 -07:00
Leonardo de Moura
f4433f3147
feat: add Alternative (StateRefT' ω σ m)
2021-08-10 14:27:05 -07:00
Leonardo de Moura
a821dcbff2
chore: enforce naming convention for theorems
...
see issue #402
fix: `ElabTerm.lean`
2021-08-07 12:48:38 -07:00
Leonardo de Moura
4dbb3e6db1
fix: add workaround to prevent code explosion at deriving for FromJson
...
fixes #569
2021-08-05 06:58:07 -07: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
Leonardo de Moura
f4a7ffd8c8
chore: fix codebase and tests
2021-06-29 17:14:52 -07:00
Leonardo de Moura
97ac231138
feat: add missing OptionT instance
2021-05-31 16:37:18 -07:00
Sebastian Ullrich
a02c6fd3eb
chore: adapt stdlib & tests
2021-05-20 15:17:36 -07:00
Leonardo de Moura
d9273786c7
chore: remove when and «unless»
...
They are obsolete.
cc @Kha
2021-03-20 18:52:18 -07:00
Leonardo de Moura
04e3f21783
chore: add OptionM monad
...
Motivation: `Option` is data, `OptionM` is control.
2021-03-20 17:50:45 -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
228bc2dd54
refactor: Traversable => ForM
2021-03-02 06:22:22 -08:00
Leonardo de Moura
81ba5485dd
refactor: StateCpsT
...
Define `run` and `run'` using `runK`.
Write auxiliary simp lemmas using `runK`.
2021-03-02 06:22:22 -08:00
Leonardo de Moura
bbf158005f
chore: make sure it matches the paper
2021-02-28 17:57:00 -08:00
Leonardo de Moura
35e1f5ad97
refactor: Foldable => Traversable
2021-02-28 16:11:20 -08:00
Leonardo de Moura
ef4d5950ae
feat: add Foldable typeclass
...
We use it in the "`do` unchained" paper.
It will eventually replace `ForIn`.
2021-02-28 09:00:52 -08:00
Leonardo de Moura
f9483a8068
feat: add ExceptCpsT.runCatch
2021-02-27 18:59:58 -08:00
Leonardo de Moura
481189bcf4
feat: add ExceptCpsT
2021-02-27 18:44:24 -08:00
