structure Cvc.ETerm : Type

Type-erased version Term.

• srt : Srt

  Sort of the underlying typed-term.

• typed : Term self.srt.toType

  Typed version of a type-erased term.

structure Cvc.EValue : Type

An erased value for some Srt.

• srt : Srt

  Sort of the value.

• val : Value self.srt.toType

  Underlying typed value as a Term.

def Cvc.ETerm.ofTerm {α : Type} [A : IsSrt α] (term : Term α) : ETerm

Constructor from a typed term.

Equations

• Cvc.ETerm.ofTerm term = { srt := Cvc.IsSrt.srt α, typed := ⋯ ▸ term }

def Cvc.ETerm.toString (erased : ETerm) : String

String representation.

Equations

• erased.toString = toString erased.typed

instance Cvc.ETerm.instToString : ToString ETerm

Equations

• Cvc.ETerm.instToString = { toString := Cvc.ETerm.toString }

def Cvc.ETerm.asSrt? (erased : ETerm) (srt : Srt) : Option (Term srt.toType)

Attempts to Srt-type an erased term.

Equations

• { srt := termSrt, typed := term }.asSrt? srt = if h_srt : termSrt = srt then some (h_srt ▸ term) else none

def Cvc.ETerm.asSrt (erased : ETerm) (srt : Srt) : Res (Term srt.toType)

Attempts to Srt-type an erased term.

Equations

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

def Cvc.ETerm.as? (erased : ETerm) (α : Type) [A : IsSrt α] : Option (Term α)

Attempts to retype an erased term.

Equations

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

def Cvc.ETerm.as (erased : ETerm) (α : Type) [A : IsSrt α] : Res (Term α)

Attempts to retype an erased term.

Equations

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

def Cvc.ETerm.getValue (erased : ETerm) : Smt.Sat EValue

Retrieve the erased value of an erased term.

Equations

• { srt := termSrt, typed := term }.getValue = do let val ← Cvc.Smt.getValue term pure { srt := termSrt, val := val }

def Cvc.Term.erase {α : Type} [IsSrt α] : Term α → ETerm

Erases the type of a typed term.

Equations

• Cvc.Term.erase = Cvc.ETerm.ofTerm

def Cvc.Term.ofErased? {α : Type} [A : IsSrt α] (erased : ETerm) : Option (Term α)

Attempts to retype an erased term.

Equations

• Cvc.Term.ofErased? erased = erased.as? α

def Cvc.Term.ofErased {α : Type} [A : IsSrt α] (erased : ETerm) : Res (Term α)

Attempts to retype an erased term.

Equations

• Cvc.Term.ofErased erased = erased.as α