Notation typeclass for well-formedness.

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

• One or more equations did not get rendered due to their size.