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

607 commits

Author SHA1 Message Date
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
Mario Carneiro
b948a56196 chore: remove [Inhabited A] from binSearch / binInsert 2022-11-13 15:00:26 -08:00
Alex J. Best
c72cf24694 chore: protect Int.repr 2022-11-13 15:00:08 -08:00
Mario Carneiro
7358df2f7e chore: remove Int.natMod 2022-11-13 14:59:26 -08:00
Sebastian Ullrich
7410d00678 feat: Subarray.findRev? 2022-11-11 09:13:02 +01:00
Leonardo de Moura
3e33fcc4f8 chore: use lean_string_utf8_next_fast 2022-11-09 12:06:37 -08:00
Leonardo de Moura
92c03c0050 perf: prepare do add String.next' 2022-11-09 12:00:31 -08:00
Leonardo de Moura
20eeb4202f perf: fast String.get' without runtime bounds check 
TODO: naming convention `String.get'` should be called `String.get`,
and we should rename the old `String.get`
 2022-11-09 12:00:30 -08:00
Leonardo de Moura
b63eb886ce chore: incorrect annotation 2022-11-07 16:18:36 -08:00
Leonardo de Moura
b8f4a345f1 feat: add Power2 2022-10-27 18:11:20 -07:00
Leonardo de Moura
e55badef05 feat: List.mapMono 2022-10-24 19:50:09 -07:00
Mario Carneiro
d7d61bfb55 feat: use withoutPosition consistently (part 2) 2022-10-24 12:51:32 -07:00