batteries
batteries copied to clipboard
leanprover-community
The "batteries included" extended library for the Lean programming language and theorem prover
Right now without the respective reverse chunks functions to check if this API design is fine before doing it wrong twice.
The linter fails here, but I claim it should succeed: ```lean import Std @[simp] theorem cast_fin_h {n m : Nat} (h : m = n) (a : Fin (m +...
Adds `getBinderPredOfProp` to query for inverse of `satisfies_binder_pred%` and extends `binder_predicate` notation to support this. This can be used in pretty printers that make use of extended binders, but this...
To ease new contributions, we should write down the style rules (indentation, usage of trailing punctuation and structuring tactics) so that we have a place to point contributors to. Currently...
As part of helping new users, we should codify naming conventions for theorems in the standard library. Related discussions: * See [this comment](https://github.com/leanprover/std4/pull/329#issuecomment-1786193983) in #329.
The current induction code action is really nice, but it doesn't work when using a non-default induction rule.
This repo is upstream from Mathlib, but we'd like to ensure changes to `main` do not break Mathlib. Should we add a build step or task that builds Mathlib (perhaps...
As of #301, we will have both `List.sublists` and `List.sublistsFast`, where the former is `implemented_by` the latter. The proof that this is safe, `sublists_eq_sublistsFast`, as of https://github.com/leanprover-community/mathlib4/pull/7746 lives in mathlib....
MWE: ```lean import Std def foo : Nat → Nat := sorry theorem foo_eq_iff (z : Nat) : z = 17 ↔ foo z = 3 := sorry theorem fail...
Metadata
Owner
Metadata
The "batteries included" extended library for the Lean programming language and theorem prover