Junyan Xu
2aeeed13cf
fix: generalize Prod.lexAccessible to match Lean 3 ( #2388 )
...
* fix: generalize Prod.lexAccessible to match Lean 3
* fix
* fix
2023-08-09 08:54:53 -07:00
Marcus Rossel
8af25455ae
doc: fix comment for Nat.sub
2023-08-09 08:54:24 -07:00
tydeu
c79c7c89b3
feat: IO.Process.getPID & IO.FS.Mode.writeNew
2023-08-08 16:23:43 -04:00
Siddharth
b9ec36d089
chore: get rid of all inline C annotations for LLVM ( #2363 )
2023-07-30 10:39:40 +02:00
Mario Carneiro
776bff1948
fix: repeat conv should not auto-close the goal
2023-07-27 18:15:35 -04:00
Bulhwi Cha
3b6bc4a87d
style: remove unnecessary space characters
2023-07-23 16:11:11 +02:00
Mario Carneiro
dd313c6894
feat: add IO.FS.rename
2023-07-22 23:21:32 +02:00
Bulhwi Cha
7809d49a62
doc: fix type signature of Coe
2023-07-22 14:16:21 +02:00
Bulhwi Cha
367b38701f
refactor: simplify String.splitOnAux ( #2271 )
2023-07-19 11:50:27 +00:00
F. G. Dorais
d10e3da673
fix: protect sizeOf lemmas
2023-07-19 08:50:59 +02:00
Floris van Doorn
1a6663a41b
chore: write "|-" as "|" noWs "-" ( #2299 )
...
* remove |- as an alias for ⊢
* revert false positive |->
* fix docstring
* undo previous changes
* [unchecked] use suggestion
* next attempt
* add test
2023-07-14 09:48:20 -07: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
Scott Morrison
60b8fdd8d6
feat: use nat_pow in the kernel
2023-07-10 09:01:14 -07:00
Sebastian Ullrich
9901804a49
feat: SpawnArgs.setsid, Child.kill
2023-07-05 23:42:53 +02:00
Leonardo de Moura
32d5def5b8
feat: add bne_iff_ne
2023-07-05 08:51:34 -07:00
Mario Carneiro
3104c223d8
fix: reference implementation for Array.mapM
2023-06-27 14:21:22 -07:00
Floris van Doorn
32e93f1dc1
fix: delete Measure and SizeOfRef ( #2275 )
...
* move Measure to Nat namespace
We could (and maybe should) also move various other declarations to namespaces, like measure. However, measure seems to be used a lot in termination_by statements, so that requires other fixes as well. Measure seems to be almost unused
* fix
* delete Measure and SizeOfRef instead
2023-06-21 22:51:28 -07:00
Bulhwi Cha
b3eeeffd90
doc: improve documentation of Init.Coe
...
Delete misleading explanations of `CoeFun` and `CoeSort`, and fix the
grammar in the documentation of `Init.Coe`.
2023-06-05 15:52:25 -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
Mario Carneiro
43f6d0a761
feat: implement have this (part 1)
2023-06-02 16:19:02 +02:00
Mario Carneiro
c20a7bf305
feat: hygieneInfo parser (aka this 2.0)
2023-06-02 16:19:02 +02:00
Mario Carneiro
e826f5f42a
fix: spacing around calc
2023-06-02 09:15:15 +02:00
Bulhwi Cha
c1a58b212a
chore: remove whitespace ( #2244 )
...
Remove a duplicate whitespace character.
2023-05-31 06:00:42 -07:00
Mario Carneiro
5661b15e35
fix: spacing and indentation fixes
2023-05-28 18:48:36 -07:00
Mario Carneiro
01ba75661e
fix: implement String.toName using decodeNameLit
...
fixes #2231
2023-05-28 17:38:57 -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
Bulhwi Cha
445fd417be
doc: add more explanations of quotients
...
Add explanations of `Quotient.ind` and `Quotient.inductionOn` to
`Init.Core`.
2023-05-05 12:22:59 -07:00
Bulhwi Cha
9fd1aeb0d8
fix: change the type of Quotient.ind
...
Change the type of `Quotient.ind` by changing the type of `q` from
`Quot Setoid.r` to `Quotient s`.
2023-05-05 12:22:59 -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
Bulhwi Cha
401e9868f8
doc: uncapitalize a letter
...
"this Type" should be "this type".
2023-05-05 12:04:35 -07:00
Scott Morrison
ac7c447855
chore: update src/Init/Tactics.lean
2023-04-19 07:15:08 -07:00
Scott Morrison
96969363e6
chore: modify misleading doc-string for repeat tactic
2023-04-18 15:56:49 +02:00
Scott Morrison
06c752448b
chore: add missing simp lemma (¬ False) = True
2023-04-10 21:05:54 -07:00
Gabriel Ebner
4af329588e
doc: clarify semi-out params
2023-04-10 13:00:04 -07:00
Gabriel Ebner
56c3e3334f
doc: semiOutParam
2023-04-10 13:00:04 -07:00
Gabriel Ebner
b8671ed18d
fix: disable checkSynthOrder for Quote instance
2023-04-10 13:00:04 -07:00
Gabriel Ebner
25fe723b14
chore: add semiOutParam annotations
2023-04-10 13:00:04 -07:00
Bulhwi Cha
d694bf2d09
doc: heading ( #2180 )
...
Add '#' to the docstring.
2023-04-03 09:40:22 +02: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
a62d412dce
fix: implement · tacs as a builtin elaborator, part 2
...
Fixes #2153
2023-03-15 17:00:15 +01:00
Sebastian Ullrich
9d144c73fd
fix: implement · tacs as a builtin elaborator
2023-03-15 13:59:16 +01:00
Sebastian Ullrich
b8cc5b277e
fix: strict indentation check in · tacs
2023-03-15 11:33:19 +01:00
