Alexander Bentkamp
Alexander Bentkamp
Hello, Is there any way to abort kernel computations without closing the session entirely?
The notation for `abs` clashes with some variants of the match notation: ``` import Mathbin.Algebra.Abs -- works if this is not imported def test : Nat → Nat | 0...
Sidekick currently does not support lambda-expressions or other binders. It seems to me that adding support for them into sidekick is the only clean way to implement the proof checker....
`Clause.proof_depth` / `Proof.Step.inferences_perfomed` considers only Inference or Simplifcation steps, but not Esa steps (e.g. Avatar). This might confuse the heuristics using it.
Our idea at the workshop was to rename `Term` into `HTerm` and `Type` into `HType`. Then the `FO` submodules can also be renamed into `HTerm`. This should be done after...
This PR defines triangular matrices based on block-triangular matrices. --- - [x] depends on: #14035 - [x] depends on: #16150 [](https://gitpod.io/from-referrer/)
Construction of a basis that triangulates a nilpotent linear map. --- [](https://gitpod.io/from-referrer/) I plan to use this result to triangularize more general matrices.
Lean4's smart unfolding relies on the markers `markSmartUnfoldigMatch` and `markSmartUnfoldigMatchAlt`. Since they are not present in mathbin definitions, definitional equality checks sometimes loop: ```lean import Mathbin.Data.Int.Basic example (n : ℕ)...
From Zulip: ~~https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/A.20set.20that.20must.20be.20a.20singletoneral.20times.2E~~ updated Link: https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/.E2.9C.94.20A.20set.20that.20must.20be.20a.20singleton This user has a weird font issue in the infoview:  Maybe this happens when the font "Source Code Pro" is not installed? This...