max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
31892 commits 1 branch 0 tags 5.3 GiB
Commit graph

618 commits

Author SHA1 Message Date
Sebastian Ullrich
dbe1c7f459 fix: make ^ a right action, add NatPow and HomogeneousPow 2023-11-12 16:57:51 +11:00
Marcus Rossel
5189578a48
doc: fix typo in Array.Mem docstring (#2856) 2023-11-10 11:16:32 +00:00
Mauricio Collares
cfe5a5f188
chore: change simp default to decide := false (#2722) 2023-11-02 10:06:38 +11:00
Parth Shastri
642bc5d8f3
fix: replace DecidableEq with BEq/LawfulBEq in List mem theorems (#2041) 2023-10-30 14:03:16 +11:00
Joachim Breitner
f74ae5f9c0
feat: Array.mem: Avoid DecidableEq, set up decreasing_trivial (#2774) 
The notation `a ∈ as` for Arrays was previously only defined with
`DecidableEq` on the elements, for (apparently) no good reason. This
drops this requirements (by using `a ∈ as.data`), and simplifies a bunch
of proofs by simply lifting the corresponding proof from lists.

Also, `sizeOf_lt_of_mem` was defined, but not set up to be picked up by
`decreasing_trivial` in the same way that the corresponding List lemma
was set up, so this adds the tactic setup.

The definition for `a ∈ as` is intentionally not defeq to `a ∈ as.data`
so that the termination tactics for Arrays don’t spuriously apply when
recursing through lists.
 2023-10-30 13:47:30 +11:00
Leonardo de Moura
b00c13a00e
chore: remove "paper cut" when using Fin USize.size (#2724) 2023-10-24 21:06:35 +11:00
Leonardo de Moura
52f1000955 chore: update doc, add support for modn 2023-10-20 19:07:48 -07:00
Leonardo de Moura
9d02e0ee6f chore: remove unnecessary % operations at Fin.mod and Fin.div 
We now have the missing proofs `Nat.mod_le` and `Nat.div_le_self` in
core.
See:
https://github.com/leanprover/std4/pull/286#discussion_r1359807875
 2023-10-20 19:07:48 -07:00
Scott Morrison
57e23917b6 fix: implementation of Array.anyMUnsafe 
move test
 2023-10-11 11:20:45 +02:00
int-y1
ce4ae37c19 chore: fix more typos in comments 2023-10-08 14:37:34 -07:00
Joachim Breitner
b2d668c340
perf: Use flat ByteArrays in Trie (#2529) 2023-09-20 13:22:37 +02:00
Scott Morrison
f1412ddb45 feat: enable failIfUnchanged by default in simp 2023-08-16 10:14:23 -07:00
Bulhwi Cha
367b38701f
refactor: simplify String.splitOnAux (#2271) 2023-07-19 11:50:27 +00:00
Leonardo de Moura
264e376741 chore: add helper function 2023-07-11 19:19:42 -07:00
Adrien Champion
d8a548fe51 chore: fix Int.div docstring examples 2023-07-10 09:09:07 -07:00
Mario Carneiro
3104c223d8 fix: reference implementation for Array.mapM 2023-06-27 14:21:22 -07:00
Mario Carneiro
bc841809c2 chore: remove intermediate 2023-06-05 15:50:11 -07:00
Mario Carneiro
2ae78f3c45 fix: tail-recursive String.foldr 2023-06-05 15:50:11 -07:00
Mario Carneiro
e68554b854 fix: use empty string instead of mk 2023-06-05 15:50:11 -07:00
Mario Carneiro
fd72fdf8f8 fix: incorrect utf8 in splitAux 2023-06-05 15:50:11 -07:00
Mario Carneiro
aa60791db3 feat: remove partial in Init.Data.String.Basic 2023-06-05 15:50:11 -07:00
Bulhwi Cha
c1a58b212a
chore: remove whitespace (#2244) 
Remove a duplicate whitespace character.
 2023-05-31 06:00:42 -07:00
Bulhwi Cha
8d0504b3b7 doc: add docstring to String.next' 2023-05-28 17:32:08 -07:00
Mario Carneiro
7f84bf07ba fix: bug in reference implementation of String.get? 2023-05-15 08:35:20 -07:00
Mario Carneiro
c9e84a6ad6 fix: remove private from string defs 2023-05-05 12:09:38 -07:00
Jakob von Raumer
45b49e7f02 fix: typos 2023-05-05 12:07:54 -07:00
Adrien Champion
39f0fa670a
doc: document Int and its basic operations (#2167) 2023-03-28 14:54:14 +02:00
Sebastian Ullrich
042d14c470 fix: List.append_eq name 
Fixes #2157
 2023-03-19 10:28:48 +01:00
Sebastian Ullrich
18297d8d91 fix: notation unexpander on overapplication of non-nullary notation 2023-01-26 13:05:33 +01:00
Eric Wieser
8cd9ce0684 refactor: redefine Nat.mod such that rfl : 0 % n = 0 
This property was true in Lean 3, and it was very convenient for working with `Fin n`.
 2023-01-11 09:49:58 -08: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
Chris Hughes
396fcd371b
feat Init.Data.Nat add simp attribute to mod_zero (#1932) 2023-01-09 09:43:41 -08:00
François G. Dorais
493a887cfb fix: remove unnecessary hypothesis 2023-01-09 18:20:41 +01:00
Gabriel Dahia
b9f0062a58 doc: replace maximum? in minimum? docstring 
This is my first contribution, if it can be counted as a contribution. Following the [documentation for simple fixes](https://github.com/leanprover/lean4/blob/master/CONTRIBUTING.md#simple-fixes), I opened the PR directly instead of discussing in the zulip or opening an issue. Hope that's ok.
 2023-01-05 14:02:19 -08:00
Gabriel Ebner
0d598dcfdf fix: Format.align always prints whitespace 2022-12-21 22:54:42 +01:00
Gabriel Ebner
eeab2af7ae fix: remove Inhabited Environment instance 2022-12-21 20:08:08 +01:00
Gabriel Ebner
14f8ff1642 feat: add CoeOut class 2022-12-21 04:24:39 +01:00
Gabriel Ebner
c7fb3a1c91 chore: make use of CoeHead chaining 2022-12-21 04:24:39 +01:00
Gabriel Ebner
f3f4eba945 fix: make Format.*join* tail-recursive 2022-12-12 22:58:21 +01:00
Gabriel Ebner
1c8ef51124 fix: make List.toString tail-recursive 2022-12-12 22:58:21 +01:00
Mario Carneiro
eb3b0377d7 fix: List.groupBy 2022-12-12 16:55:27 +01:00
Gabriel Ebner
681bbe5cf4 feat: ByteArray.hash 2022-12-01 20:18:14 -08:00
Henrik Böving
24cc6eae6d feat: log2 for Fin and UInts 2022-11-29 01:05:06 +01:00
Mario Carneiro
17ef0cea8a feat: intra-line withPosition formatting 2022-11-28 09:02:08 -08:00
Leonardo de Moura
9dbd9ec554 chore: fix build 2022-11-28 07:53:43 -08:00
Mario Carneiro
c8859a31d9 fix: Nat.log2_terminates should not be private 2022-11-19 08:26:59 -08:00
Mario Carneiro
f74fee07e6
doc: document Init.Data.List.Basic (#1828) 
* doc: document Init.Data.List.Basic

* Apply suggestions from code review

Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>

Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
 2022-11-18 06:16:50 -08:00
Sebastian Ullrich
a4abbf07b8 chore: remove remnants of C++ format 2022-11-18 06:11:24 -08:00
Leonardo de Moura
a4acf084c8 chore: fix build 2022-11-15 16:51:40 -08:00
Mario Carneiro
a2199d6d57 doc: document Init.Data.Nat.Basic 2022-11-13 21:59:57 -08:00