class Cslib.HasContext (Term : Sort u_1) : Sort (max u_1 (u_2 + 1))

Class for types (Term) that have a notion of (single-hole) contexts (Context).

• Context : Sort u_2

  The type of contexts.

• fill (c : Context Term) (t : Term) : Term

  Replaces the hole in the context with a term.

def Cslib.«term_[_]» : Lean.TrailingParserDescr

Replaces the hole in the context with a term.

Equations

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