Mario Carneiro
aa60791db3
feat: remove partial in Init.Data.String.Basic
2023-06-05 15:50:11 -07:00
Sebastian Ullrich
18297d8d91
fix: notation unexpander on overapplication of non-nullary notation
2023-01-26 13:05:33 +01:00
Bulhwi Cha
99662c1b45
chore: rename le_or_eq_or_le_succ ( #2024 )
...
Rename `le_or_eq_or_le_succ` `le_or_eq_of_le_succ`. We need to change
its name in `Std/Data/Array/Init/Lemmas` and `Std/Data/Array/Lemmas`.
Co-authored-by: Bulhwi Cha <chabulhwi@semmalgil.com>
2023-01-09 09:45:51 -08:00
Mario Carneiro
a2199d6d57
doc: document Init.Data.Nat.Basic
2022-11-13 21:59:57 -08:00
Leonardo de Moura
b8f4a345f1
feat: add Power2
2022-10-27 18:11:20 -07:00
Gabriel Ebner
fc304d95c0
feat: Min/Max typeclasses
2022-10-21 14:36:38 -07:00
Mario Carneiro
ce3c0c0e6b
feat: add TR versions of Nat.{fold, any, all, repeat}
2022-08-31 17:52:59 -07:00
Mario Carneiro
f6211b1a74
chore: convert doc/mod comments from /- to /--//-! ( #1354 )
2022-07-22 12:05:31 -07:00
François G. Dorais
bc206b2992
fix: LawfulBEq class
...
make arguments implicit and protect `LawfulBEq.rfl`
2022-06-16 15:33:32 -07:00
Wojciech Nawrocki
ff15e31e85
refactor: remove redundant theorem
2022-06-12 14:01:05 -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
François G. Dorais
155b41937a
fix: remove unnecessary hypothesis ( #1144 )
2022-05-07 15:39:37 -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
4ab57475a0
chore: simplify proofs
2022-04-23 12:47:10 -07:00
Leonardo de Moura
2a36ae4627
feat: add List.le_antisymm
2022-04-20 16:31:25 -07:00
Leonardo de Moura
8636594dac
chore: add [simp] to Nat.lt_irrefl
2022-04-01 18:50:32 -07:00
Leonardo de Moura
c6dae18787
chore: add helper theorems
2022-03-14 16:24:05 -07:00
Leonardo de Moura
14ed473777
feat: mark Nat.zero_le as simp theorem
2022-03-14 15:19:52 -07:00
Leonardo de Moura
f629be745b
chore: add Nat.le_refl as simp theorem
2022-03-03 17:18:11 -08:00
Leonardo de Moura
de51160929
fix: core library
2022-03-01 13:36:24 -08:00
François G. Dorais
e84699f130
fix: remove unnecessary hypotheses
2022-03-01 13:31:01 -08:00
Leonardo de Moura
0f796ac804
chore: avoid heterogeneous polymorphic operations and add add hugeFuel at Linear.lean
2022-03-01 11:25:15 -08:00
Leonardo de Moura
da55789c26
feat: add a proper BEq instance for Nat
2022-03-01 09:01:08 -08:00
Leonardo de Moura
0f06fbf648
feat: LawfulBEq must be reflexive
2022-02-28 19:27:51 -08:00
Leonardo de Moura
e8fb0c96ac
feat: add helper theorems
2022-02-28 18:06:02 -08:00
Leonardo de Moura
812cc72285
chore: add helper theorems
2022-02-25 17:04:04 -08:00
Leonardo de Moura
05be43455a
feat: add src/Init/Data/Nat/Linear.lean
2022-02-24 13:45:17 -08:00
Leonardo de Moura
8d6750469e
chore: helper Nat theorems
2022-02-22 14:26:50 -08:00
Leonardo de Moura
7f3a3138d0
feat: helper Nat theorems
2022-02-21 08:49:50 -08:00
Leonardo de Moura
ba16903205
feat: add helper theorems
2022-02-19 21:25:44 -08:00
Leonardo de Moura
193859c72c
feat: add helper theorems
2022-02-19 17:53:54 -08:00
Leonardo de Moura
6b6c44c559
feat: add helper lemma
2022-02-10 16:51:32 -08:00
Leonardo de Moura
dae3489fe2
feat: remove partials from Init/Data/Array/Basic.lean
2022-01-10 16:05:33 -08:00
Leonardo de Moura
0dd3ce0598
chore: fix test
2022-01-10 14:31:23 -08:00
Leonardo de Moura
16b4aa81e5
chore: add helper lemmas for well-founded recursion
2022-01-10 14:07:35 -08:00
Leonardo de Moura
241db0fed6
chore: fix name
2022-01-10 13:20:49 -08:00
Leonardo de Moura
4e70a20292
feat: add more Nat "re-packing" simp theorems
2021-10-19 06:43:07 -07:00
Leonardo de Moura
2fd024c26f
feat: add support for foldlM, foldl, ForIn instances for byte/float arrays
2021-10-18 16:54:56 -07:00
Leonardo de Moura
9d0fe5cbf9
chore: add simp rule Nat.lt x y = (x < y)
2021-10-06 16:37:58 -07:00
Leonardo de Moura
9032ddd773
chore: add simp lemma for converting Nat.add back into + notation
2021-09-08 14:58:13 -07:00
Leonardo de Moura
2a6473641a
chore: fix theorem name
2021-08-30 10:10:54 -07:00
Leonardo de Moura
00193fb953
feat: add theorems for tutorial
2021-08-26 12:13:15 -07:00
Leonardo de Moura
795ccf6e2b
chore: add Trans instances for tutorial
2021-08-25 08:50:51 -07:00
Leonardo de Moura
f08b542068
chore: add Nat.add_mul and Nat.mul_add for tutorial
2021-08-25 06:44:12 -07:00
Leonardo de Moura
7066619123
refactor: define Nat.le using inductive type
2021-08-20 19:39:45 -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
f4a7ffd8c8
chore: fix codebase and tests
2021-06-29 17:14:52 -07:00
Sebastian Ullrich
a02c6fd3eb
chore: adapt stdlib & tests
2021-05-20 15:17:36 -07:00
Leonardo de Moura
c7096f54a2
feat: injectivity theorems for types defined in the prelude
2021-05-14 18:32:26 -07:00
