lean4

lean4 copied to clipboard

Should `.below` be marked as private/internal?

4

See for example ``` #check List.Sublist.below.cons List.Sublist.below.cons.{u_1} {α : Type u_1} : ∀ {motive : (a a_1 : List α) → a.Sublist a_1 → Prop} {l₁ l₂ : List α}...

kim-em

fix: do not ban `..` with a `.` on the next line

3

Without this change, ```lean example : True := by refine' trivial .. . trivial ``` is a parse error. # Read this section before submitting * Ensure your PR follows...

eric-wieser

default value of structure which is not produced by a tactic

1

### Description constructor of structure does not accept defalut value of field whose type is not `Prop`. ```lean structure NonEmptyString where value : String another_value : Int := 0 ev...

Seasawher

### Prerequisites Please put an X between the brackets as you perform the following steps: * [X] Check that your issue is not already filed: https://github.com/leanprover/lean4/issues * [X] Reduce the...

JLimperg

Can't add local attribute for namespaced theorem

1

### Prerequisites Please put an X between the brackets as you perform the following steps: * [X] Check that your issue is not already filed: https://github.com/leanprover/lean4/issues * [X] Reduce the...

JLimperg

MWE: ```lean import Lean elab (ident)? ("Foo") : command => sorry syntax "Fix " colGt ident : tactic example (x : Lean.TSyntax `ident) : Lean.MacroM Lean.Syntax := `(tactic| Fix $x:iden)...

digama0

### Prerequisites Please put an X between the brackets as you perform the following steps: * [x] Check that your issue is not already filed: https://github.com/leanprover/lean4/issues * [x] Reduce the...

JamesGallicchio

### Prerequisites Please put an X between the brackets as you perform the following steps: * [x] Check that your issue is not already filed: https://github.com/leanprover/lean4/issues * [x] Reduce the...

llllvvuu

feat: ship cadical

2

Kha

feat: display auto-implicits as inlay hints

3

Kha