class Cslib.HasWellFormed (α : Type u) : Type u

Typeclass for types equipped with a well-formedness predicate.

• wf (x : α) : Prop

  Establishes whether x is well-formed.

def Cslib.«term_✓» : Lean.TrailingParserDescr

Notation for well-formedness.

Equations

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