Leonardo de Moura
c54a7c8ccc
chore: make HasEquiv more general
2021-03-13 07:02:35 -08:00
Leonardo de Moura
a30a256123
refactor: remove Tactic/Binders.lean
...
These macro expansion functions can be now implemented using `macro` and `macro_rules`.
2021-03-12 17:59:21 -08:00
Leonardo de Moura
d330f1e2e2
feat: rotateLeft and rotateRight tactics
2021-03-12 17:13:03 -08:00
Leonardo de Moura
091fadbf64
feat: add List.rotateLeft and List.rotateRight
2021-03-12 17:09:22 -08:00
Leonardo de Moura
3d58c4d115
chore: remove old notation
2021-03-12 15:05:06 -08:00
Leonardo de Moura
bf8119a5cd
chore: convert keywords to snake_case
...
Again `!` is only for functions that can panic.
2021-03-12 13:34:51 -08:00
Leonardo de Moura
472c5fb900
fix: indentation issues
2021-03-12 11:09:28 -08:00
Leonardo de Moura
df994fd16f
fix: add checkColGe to matchAlt
...
@Kha this is a fix for the example that @gebner posted on Zulip.
There are other possible workarounds, but I think this one is
"intuitive".
Here is the problem description and workaround.
We currently use the `withPosition` combinator at `matchAlts`. The
original motivation was nested `match`-expressions without
parenthesis.
We also have the `checkColGt` in the application parser.
Thus, `frob 5` is not parsed as an application. That is, the term
parser after the `then` keyword stops at `frob`.
Then, we get the weird "expected 'else'" error message at `5` :)
In this commit, I add a `checkColGe` check at the beginning of each
alternative right-hand-side.
The effect on the stdlib was minimal. It basically affected old code
that used the Lean 3 workaround for partial functions
```
partial def f : N -> N | i =>
...
```
In Lean 4, we can use the more natural
```
partial def f (i : N) : N :=
...
```
or
```
partial def f : N -> N := fun i =>
...
```
It also affected code such as
```
instance : Repr String.Iterator where
reprPrec | ⟨s, pos⟩, prec =>
Repr.addAppParen ("String.Iterator.mk " ++ reprArg s ++ " " ++ reprArg pos) prec
```
This is a workaround for a missing feature. We really wanted to write
```
instance : Repr String.Iterator where
reprPrec ⟨s, pos⟩ prec :=
Repr.addAppParen ("String.Iterator.mk " ++ reprArg s ++ " " ++ reprArg pos) prec
```
2021-03-12 11:06:07 -08:00
Leonardo de Moura
1112ab6eff
chore: use new notation
2021-03-11 11:19:33 -08:00
Leonardo de Moura
e7140959c4
chore: add elaborator for let_fun and let_delayed
2021-03-11 10:40:25 -08:00
Leonardo de Moura
9f88ea8047
chore: remove old decide!, nativeRefl!, and nativeDecide!
2021-03-11 08:06:20 -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
9901898258
feat: add Nat.gcd
...
This commit also fix some theorem names to new naming convention.
2021-03-07 18:47:02 -08:00
Leonardo de Moura
51e7f45af2
refactor: cases
...
remove dead `induction/cases` code
2021-03-07 12:37:02 -08:00
Leonardo de Moura
e5f1bd2eb9
chore: fix Core.lean
2021-03-07 12:08:37 -08:00
Leonardo de Moura
55115a4a1b
feat: add inferInstance tactic
2021-03-07 12:08:25 -08:00
Leonardo de Moura
dfa5cf9282
chore: add optional preprocessing tactic
2021-03-07 12:03:54 -08:00
Leonardo de Moura
66f1a88f2c
feat: simp [-decl]
2021-03-04 17:50:44 -08:00
Joe Hendrix
9bd60c7519
feat: Nat/Fin/UInt instances of bitwise classes
2021-03-04 15:42:43 -08:00
Joe Hendrix
2831dd6872
feat: Bitwise classes using F# notation.
2021-03-04 15:40:12 -08:00
Leonardo de Moura
1fedbfb9a3
feat: simp only
2021-03-04 11:58:34 -08:00
Leonardo de Moura
130a087ecf
feat: Lean 3 french single quote notation
2021-03-04 09:43:59 -08:00
Leonardo de Moura
e841f16738
fix: typo in theorem
...
`()` is `Unit`
2021-03-03 19:50:11 -08:00
Leonardo de Moura
3107473c9f
feat: add rename tactic
...
cc @Kha
2021-03-03 18:32:25 -08:00
Leonardo de Moura
6cdc6cb1d0
feat: add contradiction
2021-03-03 17:00:54 -08:00
Leonardo de Moura
4aec7579db
test: add do equivalence examples
2021-03-03 13:44:30 -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
9d9f14cd5e
chore: mark List.foldlM as protected
2021-02-28 09:14:37 -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
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
