structure Cvc.ESymbol (R : Symbol.Repr := fun (x : Type) [IsSrt x] => Symbol.Ident x) : Type

• srt : Srt
• getData : R self.srt.toType

@[reducible, inline]

abbrev Cvc.ESymbol.type {R : Symbol.Repr} (erased : ESymbol R) : Type

Equations

• erased.type = erased.srt.toType

def Cvc.ESymbol.mapM {R : Symbol.Repr} (erased : ESymbol R) {m : Type → Type u_1} {R' : Symbol.Repr} [Monad m] (f : R erased.srt.toType → m (R' erased.srt.toType)) : m (ESymbol R')

Equations

• erased.mapM f = do let __do_lift ← f erased.getData pure { srt := erased.srt, getData := __do_lift }

def Cvc.ESymbol.map {R : Symbol.Repr} (erased : ESymbol R) {R' : Symbol.Repr} (f : R erased.srt.toType → R' erased.srt.toType) : ESymbol R'

Equations

• erased.map f = erased.mapM f

@[reducible, inline]

abbrev Cvc.ESymbol.Ident : Type

Equations

• Cvc.ESymbol.Ident = Cvc.ESymbol

@[reducible, inline]

abbrev Cvc.ESymbol.Term : Type

Equations

• Cvc.ESymbol.Term = Cvc.ESymbol fun (x : Type) [Cvc.IsSrt x] => Cvc.Symbol.Term x

@[reducible, inline]

abbrev Cvc.ESymbol.Value : Type

Equations

• Cvc.ESymbol.Value = Cvc.ESymbol fun (x : Type) [Cvc.IsSrt x] => Cvc.Symbol.Value x

def Cvc.ESymbol.toString {R : Symbol.Repr} (symbol : ESymbol R) [ToString (R symbol.srt.toType)] : String

Equations

• symbol.toString = toString symbol.getData

instance Cvc.ESymbol.instToStringIdent : ToString ESymbol.Ident

Equations

• Cvc.ESymbol.instToStringIdent = { toString := fun (x : Cvc.ESymbol.Ident) => Cvc.ESymbol.toString x }

instance Cvc.ESymbol.instToStringTerm : ToString ESymbol.Term

Equations

• Cvc.ESymbol.instToStringTerm = { toString := fun (x : Cvc.ESymbol.Term) => Cvc.ESymbol.toString x }

instance Cvc.ESymbol.instToStringValue : ToString ESymbol.Value

Equations

• Cvc.ESymbol.instToStringValue = { toString := fun (x : Cvc.ESymbol.Value) => Cvc.ESymbol.toString x }

def Cvc.ESymbol.mkIdent (name : String) (α : Type) [IsSrt α] : ESymbol.Ident

Equations

• Cvc.ESymbol.mkIdent name α = { srt := Cvc.getSrt α, getData := Cvc.Symbol.Ident.mk name }

def Cvc.ESymbol.Ident.mk (name : String) (α : Type) [IsSrt α] : ESymbol.Ident

Equations

• Cvc.ESymbol.Ident.mk = Cvc.ESymbol.mkIdent

def Cvc.ESymbol.Ident.declare (ident : ESymbol.Ident) : Smt ESymbol.Term

Equations

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

def Cvc.ESymbol.Term.toTerm (term : ESymbol.Term) : Term term.srt.toType

Equations

• term.toTerm = term.getData.get

def Cvc.ESymbol.Term.toETerm (term : ESymbol.Term) : ETerm

Equations

• term.toETerm = { srt := term.srt, typed := term.toTerm }

instance Cvc.ESymbol.Term.instCoeETerm : Coe ESymbol.Term ETerm

Equations

• Cvc.ESymbol.Term.instCoeETerm = { coe := Cvc.ESymbol.Term.toETerm }

def Cvc.ESymbol.Term.getValue (term : ESymbol.Term) : Smt.Sat ESymbol.Value

Equations

• term.getValue = do let __do_lift ← Cvc.Symbol.getValue term.getData pure { srt := term.srt, getData := __do_lift }

def Cvc.ESymbol.Value.toValue (value : ESymbol.Value) : Value value.srt.toType

Equations

• value.toValue = value.getData.get

def Cvc.ESymbol.Value.toEValue (value : ESymbol.Value) : EValue

Equations

• value.toEValue = { srt := value.srt, val := value.toValue }

instance Cvc.ESymbol.Value.instCoeEValue : Coe ESymbol.Value EValue

Equations

• Cvc.ESymbol.Value.instCoeEValue = { coe := Cvc.ESymbol.Value.toEValue }

structure Cvc.ESymbols.ByName (R : Symbol.Repr) : Type

• ofRBMap :: (
• rbMap : RBMap String (ESymbol R)
• )

def Cvc.ESymbols.ByName.mapM {m : Type → Type u_1} {R R' : Symbol.Repr} [Monad m] (symbols : ByName R) (f : (srt : Srt) → R srt.toType → m (R' srt.toType)) : m (ByName R')

Equations

• symbols.mapM f = Cvc.ESymbols.ByName.ofRBMap <$> Cvc.RBMap.mapValM (fun (_name : String) (symbol : Cvc.ESymbol R) => symbol.mapM (f symbol.srt)) symbols.rbMap

def Cvc.ESymbols.ByName.map {R R' : Symbol.Repr} (symbols : ByName R) (f : (srt : Srt) → R srt.toType → R' srt.toType) : ByName R'

Equations

• symbols.map f = symbols.mapM f

def Cvc.ESymbols.ByName.forIn {m : Type u_1 → Type u_2} {R : Symbol.Repr} {β : Type u_1} [Monad m] (symbols : ByName R) (init : β) (f : (srt : Srt) → R srt.toType → β → m (ForInStep β)) : m β

Equations

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

instance Cvc.ESymbols.ByName.instSymbols : Symbols ByName

Equations

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

@[reducible, inline]

abbrev Cvc.ESymbols.ByName.Idents : Type

Equations

• Cvc.ESymbols.ByName.Idents = Cvc.Symbols.Idents

@[reducible, inline]

abbrev Cvc.ESymbols.ByName.Terms : Type

Equations

• Cvc.ESymbols.ByName.Terms = Cvc.Symbols.Terms

@[reducible, inline]

abbrev Cvc.ESymbols.ByName.Values : Type

Equations

• Cvc.ESymbols.ByName.Values = Cvc.Symbols.Values

@[reducible, inline]

abbrev Cvc.ESymbols.ByName.RelT (m : Type → Type u_1) : Type u_1

Equations

• Cvc.ESymbols.ByName.RelT m = (Cvc.ESymbols.ByName.Terms → Cvc.ESymbols.ByName.PredT m)

@[reducible, inline]

abbrev Cvc.ESymbols.ByName.PredicateT (m : Type → Type u_1) : Type u_1

Equations

• Cvc.ESymbols.ByName.PredicateT m = Cvc.ESymbols.ByName.FunT m Bool

@[reducible, inline]

abbrev Cvc.ESymbols.ByName.RelationT (m : Type → Type u_1) : Type u_1

Equations

• Cvc.ESymbols.ByName.RelationT m = (Cvc.ESymbols.ByName.Terms → Cvc.ESymbols.ByName.PredT m)

@[reducible, inline]

abbrev Cvc.ESymbols.ByName.Pred : Type

Equations

• Cvc.ESymbols.ByName.Pred = Cvc.ESymbols.ByName.PredT Id

@[reducible, inline]

abbrev Cvc.ESymbols.ByName.PredT (m : Type → Type u_1) : Type u_1

Equations

• Cvc.ESymbols.ByName.PredT m = Cvc.ESymbols.ByName.FunT m Bool

@[reducible, inline]

abbrev Cvc.ESymbols.ByName.Function (α : Type) : Type

Equations

• Cvc.ESymbols.ByName.Function α = Cvc.ESymbols.ByName.FunT Id α

@[reducible, inline]

abbrev Cvc.ESymbols.ByName.FunT (m : Type → Type u_1) (α : Type) : Type u_1

Equations

• Cvc.ESymbols.ByName.FunT m α = (Cvc.ESymbols.ByName.Terms → Cvc.Term.BuildT m (Cvc.Term α))

@[reducible, inline]

abbrev Cvc.ESymbols.ByName.Rel : Type

Equations

• Cvc.ESymbols.ByName.Rel = Cvc.ESymbols.ByName.RelT Id

@[reducible, inline]

abbrev Cvc.ESymbols.ByName.FunctionT (m : Type → Type u_1) (α : Type) : Type u_1

Equations

• Cvc.ESymbols.ByName.FunctionT = Cvc.ESymbols.ByName.FunT

@[reducible, inline]

abbrev Cvc.ESymbols.ByName.Predicate : Type

Equations

• Cvc.ESymbols.ByName.Predicate = Cvc.ESymbols.ByName.PredT Id

@[reducible, inline]

abbrev Cvc.ESymbols.ByName.Fun (α : Type) : Type

Equations

• Cvc.ESymbols.ByName.Fun α = Cvc.ESymbols.ByName.FunT Id α

@[reducible, inline]

abbrev Cvc.ESymbols.ByName.Relation : Type

Equations

• Cvc.ESymbols.ByName.Relation = Cvc.ESymbols.ByName.RelT Id

def Cvc.ESymbols.ByName.empty {R : Symbol.Repr} : ByName R

Equations

• Cvc.ESymbols.ByName.empty = { rbMap := Cvc.RBMap.empty }

def Cvc.ESymbols.ByName.emptyIdents : ByName.Idents

Equations

• Cvc.ESymbols.ByName.emptyIdents = Cvc.ESymbols.ByName.empty

def Cvc.ESymbols.ByName.find? {R : Symbol.Repr} (symbols : ByName R) (name : String) : Option (ESymbol R)

Equations

• symbols.find? name = Batteries.RBMap.find? symbols.rbMap name

def Cvc.ESymbols.ByName.find {R : Symbol.Repr} (symbols : ByName R) (name : String) : Res (ESymbol R)

Equations

• symbols.find name = match Batteries.RBMap.find? symbols.rbMap name with | some term => pure term | x => Cvc.throwUser (toString "unknown symbol `" ++ toString name ++ toString "`")

def Cvc.ESymbols.ByName.findMapOr {R : Symbol.Repr} (symbols : ByName R) {α : Sort u_1} (name : String) (f : ESymbol R → α) (getDefault : Unit → α) : α

Equations

• symbols.findMapOr name f getDefault = match symbols.find? name with | some s => f s | x => getDefault ()

def Cvc.ESymbols.ByName.findSrt? {R : Symbol.Repr} (symbols : ByName R) (name : String) : Option Srt

Equations

• symbols.findSrt? name = Option.map Cvc.ESymbol.srt (symbols.find? name)

def Cvc.ESymbols.ByName.findSrt {R : Symbol.Repr} (symbols : ByName R) (name : String) : Res Srt

Equations

• symbols.findSrt name = ExceptT.map Cvc.ESymbol.srt (symbols.find name)

def Cvc.ESymbols.ByName.findAsSrt? {R : Symbol.Repr} (symbols : ByName R) (srt : Srt) (name : String) : Option (R srt.toType)

Equations

• symbols.findAsSrt? srt name = do let __discr ← symbols.find? name match __discr with | { srt := srt', getData := repr } => if h : srt' = srt then pure (h ▸ repr) else none

def Cvc.ESymbols.ByName.findAsSrt {R : Symbol.Repr} (symbols : ByName R) (srt : Srt) (name : String) : Res (R srt.toType)

Equations

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

def Cvc.ESymbols.ByName.findMapOrAsSrt {R : Symbol.Repr} (symbols : ByName R) {α : Sort u_1} (srt : Srt) (name : String) (f : R srt.toType → α) (getDefault : Unit → α) : α

Equations

• symbols.findMapOrAsSrt srt name f getDefault = match symbols.findAsSrt? srt name with | some s => f s | x => getDefault ()

def Cvc.ESymbols.ByName.findAs? {R : Symbol.Repr} (symbols : ByName R) (α : Type) [A : IsSrt α] (name : String) : Option (R α)

Equations

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

def Cvc.ESymbols.ByName.findAs {R : Symbol.Repr} (symbols : ByName R) (α : Type) [A : IsSrt α] (name : String) : Res (R α)

Equations

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

def Cvc.ESymbols.ByName.findMapOrAs {R : Symbol.Repr} (symbols : ByName R) {β : Sort u_1} (α : Type) [A : IsSrt α] (name : String) (f : R α → β) (getDefault : Unit → β) : β

Equations

• symbols.findMapOrAs α name f getDefault = match symbols.findAs? α name with | some s => f s | x => getDefault ()

def Cvc.ESymbols.ByName.Idents.empty : ByName.Idents

Equations

• Cvc.ESymbols.ByName.Idents.empty = Cvc.ESymbols.ByName.emptyIdents

def Cvc.ESymbols.ByName.Idents.insert! (idents : ByName.Idents) (name : String) (α : Type) [A : IsSrt α] : ByName.Idents

Equations

• idents.insert! name α = Cvc.ESymbols.ByName.genericInsert!✝ idents name (Cvc.ESymbol.mkIdent name (Cvc.IsSrt.srt α).toType)

def Cvc.ESymbols.ByName.Idents.insert? (idents : ByName.Idents) (name : String) (α : Type) [A : IsSrt α] : Option ESymbol.Ident × ByName.Idents

Equations

• idents.insert? name α = Cvc.ESymbols.ByName.genericInsert?✝ idents name (Cvc.ESymbol.mkIdent name (Cvc.IsSrt.srt α).toType)

def Cvc.ESymbols.ByName.Idents.insert (idents : ByName.Idents) (name : String) (α : Type) [A : IsSrt α] : Res ByName.Idents

Equations

• idents.insert name α = Cvc.ESymbols.ByName.genericInsert✝ idents name (Cvc.ESymbol.mkIdent name (Cvc.IsSrt.srt α).toType)

def Cvc.ESymbols.ByName.Terms.find? (terms : ByName.Terms) (name : String) : Option ESymbol.Term

Equations

• terms.find? name = Cvc.ESymbols.ByName.find? terms name

def Cvc.ESymbols.ByName.Terms.find (terms : ByName.Terms) (name : String) : Res ESymbol.Term

Equations

• terms.find name = Cvc.ESymbols.ByName.find terms name

def Cvc.ESymbols.ByName.Terms.findETerm? (terms : ByName.Terms) (name : String) : Option ETerm

Equations

• terms.findETerm? name = Cvc.ESymbol.Term.toETerm <$> terms.find? name

def Cvc.ESymbols.ByName.Terms.findETerm (terms : ByName.Terms) (name : String) : Res ETerm

Equations

• terms.findETerm name = Cvc.ESymbol.Term.toETerm <$> terms.find name