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

2686 commits

Author SHA1 Message Date
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
Sebastian Ullrich
a4f732e6b1 fix: ignore vanishing files during watchdog update 2023-03-10 19:13:24 +01:00
Sebastian Ullrich
113de7cca1 refactor: move from fopen to open 2023-03-10 16:27:56 +01:00
Sebastian Ullrich
aacab14394 chore: remove support for text-mode I/O 
This didn't do anything except on Windows, where it would make the
application differ from standard Windows applications, which we don't
want.
 2023-03-10 16:27:56 +01:00
int-y1
0477276f66 chore: fix typos in prelude 2023-03-09 18:12:24 +01:00
Adrien Champion
473486eeb9 fix: calc indentation and allow underscore in first relation 2023-02-23 14:20:21 -08:00
Sebastian Ullrich
3f6c5f17db fix: unhygiene in expandExplicitBinders 2023-02-22 17:07:31 +01:00
Gabriel Ebner
3c562c1a9b fix: unify goal before executing nested tactics in calc 
Fixes #2095
 2023-02-09 11:34:07 -08:00
Sebastian Ullrich
18297d8d91 fix: notation unexpander on overapplication of non-nullary notation 2023-01-26 13:05:33 +01:00
James Gallicchio
65db25bf49
feat: funext no arg tactic (#2027) 
* feat: `funext` no arg tactic

Description of funext tactic includes behavior that is not implemented. This implements the behavior.

* fix

* feat: test new funext tactic

* use repeat for clarity of intent
 2023-01-15 08:53:49 -08: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
James Gallicchio
37650f9147
fix: add done alternative to decreasing_with (#2019) 
Previously `decreasing_with` failed if `simp_wf` closes the goal on its
own. This can cause undesired regressions when new `simp` lemmas are
introduced.

Closes #2018.
 2023-01-09 09:46:37 -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
Jeremy Salwen
60f30addc7
doc: add more detail to the split tactic docs (#1988) 
Co-authored-by: Mac <tydeu@hatpress.net>
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
 2023-01-09 13:12:39 +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
Leonardo de Moura
0739c9ccd7 chore: revert workaround 2023-01-04 09:02:02 -08:00
Gabriel Ebner
cb7657f47e fix: remove nonempty_list tactic 2023-01-03 18:17:19 -08:00
Gabriel Ebner
a2f5959118 chore: use deriving Nonempty 2022-12-22 03:48:15 +01:00
Gabriel Ebner
05401776f2 fix: add reflexivity instances to coercions 
This is important when users plug custom instances into auxiliary
classes like `CoeTC`.  We already had a reflexivity instance for
`CoeTC`.
 2022-12-22 02:02:55 +01: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
586079462c doc: explain variable conditions in type classes 2022-12-21 04:24:39 +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
78676a5a5a refactor: chain CoeHead 2022-12-21 04:24:39 +01:00