search

leanprover / lean4

Lean 4 programming language and theorem prover
https://lean-lang.org
Apache License 2.0
4.74k stars 427 forks source link

feat: allow fields in structure instance notation to have arguments #6165

Open kmill opened 4 days ago

kmill commented 4 days ago

This PR modifies structure instance notation to admit binders and type ascriptions for fields. Example:

structure PosFun where
  f : Nat → Nat
  pos : ∀ n, 0 < f n

def p : PosFun :=
  { f n := n + 1
    pos := by simp }

Just like for the structure where notation, a field f x y z : ty := val expands as f := fun x y z => (val : ty). The type ascription is optional.

leanprover-community-bot commented 4 days ago

Mathlib CI status (docs):