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

57 commits

Author SHA1 Message Date
Kim Morrison
e3811fd838
chore: cleanup unused variables (#5579) 
This pulls changes to the standard library out of #5338.
 2024-10-02 01:51:22 +00:00
Kim Morrison
d08051cf0b
chore: variables appearing on both sides of an iff should be implicit (#5254) 2024-09-04 08:33:24 +00:00
Markus Himmel
095c7b2bfc
chore: deprecate Nat.strongInductionOn (#5179) 2024-08-27 07:18:06 +00:00
Jeremy Tan Jie Rui
dd22447afd
chore: @[elab_as_elim] additions (#5147) 
This adds `@[elab_as_elim]` to `Quot.rec`, `Nat.strongInductionOn` and
`Nat.casesStrongInductionOn`, and also renames the latter two to
`Nat.strongRecOn` and `Nat.casesStrongRecOn`.

The first change resolves the todos in
[`Mathlib.Init.Quot`](ca6a6fdc07/Mathlib/Init/Quot.lean)
while the other two are based on a suggestion of @YaelDillies on [the
Zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Technical.20Debt.20Counters/near/464804567)
and related to
https://github.com/leanprover-community/mathlib4/pull/16096.
 2024-08-26 07:44:54 +00:00
Joachim Breitner
861ef27503
refactor: state WellFoundedRelation Nat using <, not Nat.lt (#5012) 
as that’s the simp normal form.
 2024-08-13 13:37:42 +00:00
Sebastian Ullrich
5da9038fb4 chore: adapt stdlib to new variable behavior 2024-08-09 11:50:54 +02:00
Kim Morrison
1cf47bce5a
chore: rename TC to Relation.TransGen (#4760) 
This is barely used in Lean, and this rename is both more readable, and
consistent with further developments downstream.

See
[zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Relation.2ETransGen.20vs.2E.20TC.20from.20Init.2ECore/near/448941824)
discussion.
 2024-07-16 17:06:49 +00:00
Kim Morrison
75e11ecf7c
chore: defs that should be theorems (#4619) 2024-07-02 03:03:11 +00:00
JovanGerb
c7c50a8bec
chore: fix linter errors (#4502) 
The linters in Batteries can be used to spot mistakes in Lean. See the
message on
[Zulip](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Go-to-def.20on.20typeclass.20fields.20and.20type-dependent.20notation/near/442613564).
These are the different linters with errors:

- unusedArguments:
There are many unused instance arguments, especially a redundant `[Monad
m]` is very common
- checkUnivs:
There was a problem with universes in a definition in
`Init.Control.StateCps`. I fixed it by adding a `variable` statement for
the implicit arguments in the file.
- defLemma:
many proofs are written as `def` instead of `theorem`, most notably
`rfl`. Because `rfl` is used as a match pattern, it must be a def. Is
this desirable?
The keyword `abbrev` is sometimes used for an alias of a theorem, which
also results in a def. I would want to replace it with the `alias`
keyword to fix this, but it isn't available.
- dupNamespace:
I fixed some of these, but left `Tactic.Tactic` and `Parser.Parser` as
they are as these seem intended.
- unusedHaveSuffices:
  I cleaned up a few proofs with unused `have` or `suffices`
- explicitVarsOfIff:
  I didn't fix any of these, because that would be a breaking change.
- simpNF:
I didn't fix any of these, because I think that requires knowing the
intended simplification order.
 2024-06-19 18:24:08 +00:00
Henrik Böving
ecba8529cc
doc: Leo-Henrik retreat doc (#3869) 
Part of the retreat Hackathon.

---------

Co-authored-by: David Thrane Christiansen <david@davidchristiansen.dk>
Co-authored-by: Mario Carneiro <di.gama@gmail.com>
 2024-04-12 09:14:31 +00:00
Leonardo de Moura
612d97440b chore: incorrectly annotated theorems 2024-03-13 12:37:58 -07:00
Scott Morrison
9cea1a503e
chore: upstream Std.Data.Prod.Lex (#3338) 2024-02-15 02:47:08 +00:00
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
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
Scott Morrison
1b50292228 chore: protect Prod.Lex 2022-11-29 20:09:08 +01:00
Adrien Champion
33aa1724f2 fix: rewrite by with strict indentation in a few struct-fields 2022-11-08 08:30:42 -08:00
Leonardo de Moura
eafd2a88ce chore: simplify Prelude.lean and Core.lean using elabAsElim 2022-07-29 18:13:56 -07:00
Leonardo de Moura
dd924e5270 chore: remove codegen option 
We should use `noncomputable` modifier instead.

closes #1288
 2022-07-07 08:18:30 -07:00
Wojciech Nawrocki
2a53857928 feat: add strong Nat induction principle 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
Leonardo de Moura
619186b2a8 feat: only use set_option codegen false where needed 2022-03-06 19:15:05 -08:00
Leonardo de Moura
3005bab970 feat: helper theorem and tactic for WF 2022-02-28 15:11:00 -08:00
Leonardo de Moura
2ba3205f94 feat: add Prod.Lex.right' 2022-02-28 11:19:28 -08:00
Leonardo de Moura
3fbf5acbee fix: add missing [reducible] annotations Init/WF.lean 2022-01-12 17:12:55 -08:00
Leonardo de Moura
1a6abe1dad feat: WellFoundedRelation as a class 2022-01-12 08:28:03 -08:00
Leonardo de Moura
ec49c31337 chore: make sure PSigma.lex signature is similar to Prod.lex 2022-01-11 14:37:53 -08:00
Leonardo de Moura
4c051896df refactor: sizeofMeasure => sizeOfWFRel 
This commit also makes the first argument of `sizeOfWFRel` implicit.
 2021-09-27 19:06:10 -07:00
Leonardo de Moura
d4509878bb feat: add WellFoundedRelation for termination_by 2021-09-25 17:21:03 -07:00
Leonardo de Moura
bb98057098 refactor: avoid wf suffix 2021-09-21 12:57:08 -07:00
Leonardo de Moura
10a38aef3c chore: remove class WellFoundedRelation 
It is dead code.
 2021-09-21 12:57:08 -07:00
Leonardo de Moura
9bb5d4dc93 chore: Nat.ltWf => Nat.lt_wf 2021-09-02 07:51:41 -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
08d865b475 chore: remove unnecessary generalizing 2021-03-27 15:03:13 -07:00
Leonardo de Moura
fba719ff02 chore: adjust WF.lean 2021-02-01 18:08:48 -08:00
Sebastian Ullrich
0c91b3769e chore: replace variables in src/ 2021-01-22 14:36:05 +01:00
Leonardo de Moura
5249fdc24d chore: cleanup and style 2020-12-12 10:36:26 -08:00
Leonardo de Moura
0869f38de4 chore: update structure, class, inductive 2020-11-27 15:09:30 -08:00
Leonardo de Moura
b72a3c69b6 fix: ambiguity at induction/cases 
See efc3a320fe
 2020-11-24 14:59:12 -08:00
Leonardo de Moura
304c80d610 feat: use <| 2020-11-19 09:03:38 -08:00
Leonardo de Moura
c305c2691f chore: use := 2020-11-19 07:22:31 -08:00
Leonardo de Moura
7e51020685 chore: move SizeOf to its own file 2020-11-10 14:43:03 -08:00
Leonardo de Moura
bf4d48f348 chore: cleanup for presentation 2020-11-05 12:43:02 -08:00
Leonardo de Moura
a6fd611db0 chore: use generalizing 2020-11-02 17:01:10 -08:00
Leonardo de Moura
a0ab1b9eb4 chore: remove with 2020-11-02 13:35:26 -08:00
Leonardo de Moura
dfc346e76f chore: remove obsolete attribute 2020-11-02 06:47:20 -08:00
Leonardo de Moura
6858cb5fb6 chore: cleanup 2020-10-29 10:24:16 -07:00
Leonardo de Moura
898a08a0c1 chore: avoid Has prefix in type classes 
closes #203
 2020-10-27 18:29:19 -07:00