class HasWellFormed (α : Type u_1) : Type u_1

Typeclass for types equipped with a well-formedness predicate.

• wf (x : α) : Prop

  Establishes whether x is well-formed.

def «term_✓» : Lean.TrailingParserDescr

Notation for well-formedness.

Equations

• «term_✓» = Lean.ParserDescr.trailingNode `«term_✓» 1022 1024 (Lean.ParserDescr.symbol "✓")