Wojciech Nawrocki
|
46257dfb0e
|
feat: show bitwise terminates
|
2022-06-12 14:01:05 -07:00 |
|
Wojciech Nawrocki
|
4d05803782
|
feat: WF lemma for Nat division
|
2022-06-12 14:01:05 -07:00 |
|
Wojciech Nawrocki
|
ff15e31e85
|
refactor: remove redundant theorem
|
2022-06-12 14:01:05 -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
|
897a5de6ac
|
chore: revert some questionable signature changes
|
2022-06-07 16:37:45 -07:00 |
|
Sebastian Ullrich
|
fb2a2b3de2
|
fix: fixup previous commit
|
2022-06-07 16:37:45 -07:00 |
|
Sebastian Ullrich
|
ae7b895f7a
|
refactor: unname some unused variables
|
2022-06-07 16:37:45 -07:00 |
|
Leonardo de Moura
|
34bbe5d12c
|
feat: add simp theorem List.of_toArray_eq_toArray (as bs : List α) : (as.toArray = bs.toArray) = (as = bs) := by
|
2022-05-27 18:26:48 -07:00 |
|
Sebastian Ullrich
|
1d44c30b3f
|
refactor: simplify log2 termination proof
|
2022-05-18 10:20:36 +02:00 |
|
François G. Dorais
|
155b41937a
|
fix: remove unnecessary hypothesis (#1144)
|
2022-05-07 15:39:37 -07:00 |
|
Leonardo de Moura
|
73cb952275
|
feat: add Hashable (Array α) instance
|
2022-05-07 15:01:32 -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 |
|
Leonardo de Moura
|
24417ed466
|
feat: size, get, get!, getD, and getOp for Subarray
|
2022-04-29 09:55:45 -07:00 |
|
Leonardo de Moura
|
cae59c6916
|
chore: remove staging workarounds
|
2022-04-26 08:23:43 -07:00 |
|
Leonardo de Moura
|
6af1da450e
|
feat: disable only eta for classes during TC resolution
closes #1123
|
2022-04-26 08:20:39 -07:00 |
|
Leonardo de Moura
|
4ab57475a0
|
chore: simplify proofs
|
2022-04-23 12:47:10 -07:00 |
|
Leonardo de Moura
|
a82abee1b2
|
feat: sum of monomials normal form by reflection
|
2022-04-22 18:51:48 -07:00 |
|
Leonardo de Moura
|
09dfd97593
|
chore: remove temporary workaround
|
2022-04-21 16:29:08 -07:00 |
|
Leonardo de Moura
|
57c3114875
|
fix: simpAll and tests
We need another `update stage0` to remove workaround at `AC.lean`
|
2022-04-21 15:00:07 -07:00 |
|
Leonardo de Moura
|
2a36ae4627
|
feat: add List.le_antisymm
|
2022-04-20 16:31:25 -07:00 |
|
Leonardo de Moura
|
bb3fc358c9
|
feat: add LawfulBEq Int instance
|
2022-04-20 14:52:41 -07:00 |
|
Leonardo de Moura
|
e3dcce5320
|
chore: remove temporary workarounds
|
2022-04-09 12:13:37 -07:00 |
|
Leonardo de Moura
|
628e33bf8a
|
feat: activate new rfl tactic implementation
|
2022-04-09 12:01:56 -07:00 |
|
Leonardo de Moura
|
de2e2447d2
|
chore: style
|
2022-04-07 17:35:05 -07:00 |
|
Leonardo de Moura
|
9d55d7bf9e
|
feat: add helper tactic for applying List.sizeOf_lt_of_mem in termination proofs
|
2022-04-02 18:38:55 -07:00 |
|
Leonardo de Moura
|
64cfbc1ae3
|
feat: add helper tactic for applying sizeOf (a.get i) < sizeOf a automatically in termination proofs
|
2022-04-02 18:29:41 -07:00 |
|
Leonardo de Moura
|
562af50191
|
feat: add ForIn' instance for Range
|
2022-04-02 18:22:21 -07:00 |
|
Leonardo de Moura
|
03ec8cb30b
|
feat: missing sizeOf theorems for Array.get and List.get
|
2022-04-02 16:04:46 -07:00 |
|
Leonardo de Moura
|
8636594dac
|
chore: add [simp] to Nat.lt_irrefl
|
2022-04-01 18:50:32 -07:00 |
|
Leonardo de Moura
|
cfb4e306f7
|
refactor: replace length_dropLast theorem
|
2022-04-01 16:44:24 -07:00 |
|
Leonardo de Moura
|
d1022e5587
|
chore: add Nat.div_add_mod
|
2022-04-01 08:20:00 -07:00 |
|
Leonardo de Moura
|
df3a8eb126
|
feat: add helper List.append simp theorems
|
2022-03-30 11:11:03 -07:00 |
|
Leonardo de Moura
|
2a37f53fca
|
chore: fix core library
|
2022-03-28 14:32:04 -07:00 |
|
Leonardo de Moura
|
87bb299f08
|
feat: add Iterator.atEnd
|
2022-03-20 11:40:46 -07:00 |
|
Leonardo de Moura
|
3862e7867b
|
refactor: make String.Pos opaque
TODO: this refactoring exposed bugs in `FuzzyMatching` and `Lake`
closes #410
|
2022-03-20 10:47:13 -07:00 |
|
casavaca
|
bf4ba1583d
|
feat: add simp theorem for List, (as.map f).length = as.length
|
2022-03-19 11:35:21 -07:00 |
|
Leonardo de Moura
|
72b6f4d528
|
chore: avoid unnecessary h :s
|
2022-03-19 11:21:37 -07:00 |
|
Leonardo de Moura
|
9fed5bda7d
|
chore: remove workarounds
|
2022-03-19 09:44:57 -07:00 |
|
Leonardo de Moura
|
4b374d4441
|
fix: Nat/Div.lean, add decreasing_with combinator, and rename decreasing_tactic_trivial
|
2022-03-19 09:40:10 -07:00 |
|
Leonardo de Moura
|
9722aeaf32
|
feat: use String.Iterator.sizeOf_next_lt in the builtin decreasing_tactic
|
2022-03-19 09:04:40 -07:00 |
|
Leonardo de Moura
|
9727387129
|
feat: helper theorem for proving termination of simple String traversal functions
|
2022-03-19 07:37:59 -07:00 |
|
Leonardo de Moura
|
64bd82dddd
|
feat: custom SizeOf instance for String.Iterator
|
2022-03-19 07:21:17 -07:00 |
|
zygi
|
ac793ce196
|
fix: forward start and stop in Array.allM
|
2022-03-17 10:08:40 +01:00 |
|
Daniel Fabian
|
cf4e873974
|
feat: support Sort u in ac_refl.
|
2022-03-16 17:21:20 -07:00 |
|
Daniel Fabian
|
d667d5ab5d
|
feat: rewrite the tactic using simp as the basis.
|
2022-03-16 17:21:20 -07:00 |
|
Daniel Fabian
|
fda1c5b192
|
refactor: simplify proof using <;>
|
2022-03-16 17:21:20 -07:00 |
|
Daniel Fabian
|
a60220b036
|
feat: add tactic for ac_refl.
|
2022-03-16 17:21:20 -07:00 |
|
Daniel Fabian
|
eaa48f0d8d
|
refactor: move ac proofs to Init.
|
2022-03-16 17:21:20 -07:00 |
|
Leonardo de Moura
|
c6dae18787
|
chore: add helper theorems
|
2022-03-14 16:24:05 -07:00 |
|