@[reducible, inline]

abbrev Cvc.Symbols.Repr : Type 1

Equations

• Cvc.Symbols.Repr = (Cvc.Symbol.Repr → Type)

class Cvc.Symbols (Struct : Symbols.Repr) : Type 1

Abstraction over an heterogeneous, strongly-typed function symbol structure.

Users will typically manipulate structures dealing with heterogeneously-typed symbols so that they can represent, for instance, the state of a transition systems. This class abstracts over such structures so that cvc.lean can provide helpers for declaring function symbols, retrieving their (strongly-typed) value, etc.

• mapM {R R' : Symbol.Repr} {m : Type → Type} [Monad m] (repr : Struct R) (f : {α : Type} → [inst : IsSrt α] → R α → m (R' α)) : m (Struct R')

  Monadic map over a Struct _.

• forIn {R : Symbol.Repr} {β : Type} {m : Type → Type} [Monad m] (symbols : Struct R) (init : β) (f : {α : Type} → [inst : IsSrt α] → R α → β → m (ForInStep β)) : m β

  ForIn-like iteration/fold over ESymbol _ elements.

def Cvc.Symbols.map {Struct : Symbols.Repr} [Syms : Symbols Struct] {R G : Symbol.Repr} (symbols : Struct R) (f : {α : Type} → [inst : IsSrt α] → R α → G α) : Struct G

Maps over the symbols in a Struct F.

Equations

• Cvc.Symbols.map symbols f = Cvc.Symbols.mapM symbols fun {α : Type} [Cvc.IsSrt α] => f

@[defaultInstance 1000]

instance Cvc.Symbols.instForIn {Struct : Symbols.Repr} [Syms : Symbols Struct] {m : Type → Type} {R : Symbol.Repr} : ForIn m (Struct R) ((α : Type) × (x : IsSrt α) × R α)

Equations

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

@[reducible, inline]

abbrev Cvc.Symbols.Idents {Struct : Symbols.Repr} [Syms : Symbols Struct] : Type

Equations

• Cvc.Symbols.Idents = Struct fun (x : Type) [Cvc.IsSrt x] => Cvc.Symbol.Ident x

@[reducible, inline]

abbrev Cvc.Symbols.Terms {Struct : Symbols.Repr} [Syms : Symbols Struct] : Type

Equations

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

@[reducible, inline]

abbrev Cvc.Symbols.Values {Struct : Symbols.Repr} [Syms : Symbols Struct] : Type

Equations

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

@[reducible, inline]

abbrev Cvc.Symbols.Model {Struct : Symbols.Repr} [Syms : Symbols Struct] : Type

Equations

• Cvc.Symbols.Model = Cvc.Symbols.Values

@[reducible, inline]

abbrev Cvc.Symbols.FunT {Struct : Symbols.Repr} [Syms : Symbols Struct] (m : Type → Type u_1) (α : Type) : Type u_1

Equations

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

@[reducible, inline]

abbrev Cvc.Symbols.FunctionT {Struct : Symbols.Repr} [Syms : Symbols Struct] (m : Type → Type u_1) (α : Type) : Type u_1

Equations

• @Cvc.Symbols.FunctionT = @Cvc.Symbols.FunT

@[reducible, inline]

abbrev Cvc.Symbols.PredT {Struct : Symbols.Repr} [Syms : Symbols Struct] (m : Type → Type u_1) : Type u_1

Equations

• Cvc.Symbols.PredT m = Cvc.Symbols.FunT m Bool

@[reducible, inline]

abbrev Cvc.Symbols.PredicateT {Struct : Symbols.Repr} [Syms : Symbols Struct] (m : Type → Type u_1) : Type u_1

Equations

• @Cvc.Symbols.PredicateT = @Cvc.Symbols.PredT

@[reducible, inline]

abbrev Cvc.Symbols.RelT {Struct : Symbols.Repr} [Syms : Symbols Struct] (m : Type → Type u_1) : Type u_1

Equations

• Cvc.Symbols.RelT m = (Cvc.Symbols.Terms → Cvc.Symbols.PredT m)

@[reducible, inline]

abbrev Cvc.Symbols.RelationT {Struct : Symbols.Repr} [Syms : Symbols Struct] (m : Type → Type u_1) : Type u_1

Equations

• @Cvc.Symbols.RelationT = @Cvc.Symbols.RelT

@[reducible, inline]

abbrev Cvc.Symbols.Fun {Struct : Symbols.Repr} [Syms : Symbols Struct] (α : Type) : Type

Equations

• Cvc.Symbols.Fun α = Cvc.Symbols.FunT Id α

@[reducible, inline]

abbrev Cvc.Symbols.Function {Struct : Symbols.Repr} [Syms : Symbols Struct] (α : Type) : Type

Equations

• @Cvc.Symbols.Function = @Cvc.Symbols.Fun

@[reducible, inline]

abbrev Cvc.Symbols.Pred {Struct : Symbols.Repr} [Syms : Symbols Struct] : Type

Equations

• Cvc.Symbols.Pred = Cvc.Symbols.PredT Id

@[reducible, inline]

abbrev Cvc.Symbols.Predicate {Struct : Symbols.Repr} [Syms : Symbols Struct] : Type

Equations

• @Cvc.Symbols.Predicate = @Cvc.Symbols.Pred

@[reducible, inline]

abbrev Cvc.Symbols.Rel {Struct : Symbols.Repr} [Syms : Symbols Struct] : Type

Equations

• Cvc.Symbols.Rel = Cvc.Symbols.RelT Id

@[reducible, inline]

abbrev Cvc.Symbols.Relation {Struct : Symbols.Repr} [Syms : Symbols Struct] : Type

Equations

• @Cvc.Symbols.Relation = @Cvc.Symbols.Rel

Ident-specific helpers

def Cvc.Symbols.Idents.mapM {Struct : Symbols.Repr} [Syms : Symbols Struct] (idents : Idents) {m : Type → Type} {R : Symbol.Repr} [Monad m] (f : {α : Type} → [inst : IsSrt α] → Symbol.Ident α → m (R α)) : m (Struct R)

Equations

• idents.mapM f = Cvc.Symbols.mapM idents fun {α : Type} [Cvc.IsSrt α] (sym : Cvc.Symbol.Ident α) => f sym

def Cvc.Symbols.Idents.map {Struct : Symbols.Repr} [Syms : Symbols Struct] (idents : Idents) {R : Symbol.Repr} (f : {α : Type} → [inst : IsSrt α] → Symbol.Ident α → R α) : Struct R

Equations

• idents.map f = idents.mapM fun {α : Type} [Cvc.IsSrt α] => f

def Cvc.Symbols.Idents.declare {Struct : Symbols.Repr} [Syms : Symbols Struct] (idents : Idents) : Smt Terms

Equations

• idents.declare = idents.mapM fun {α : Type} [Cvc.IsSrt α] (ident : Cvc.Symbol.Ident α) => Cvc.Symbol.declare ident

Term-specific helpers

def Cvc.Symbols.Terms.mapM {Struct : Symbols.Repr} [Syms : Symbols Struct] (terms : Terms) {m : Type → Type} {R : Symbol.Repr} [Monad m] (f : {α : Type} → [inst : IsSrt α] → Symbol.Term α → m (R α)) : m (Struct R)

Equations

• terms.mapM f = Cvc.Symbols.mapM terms fun {α : Type} [Cvc.IsSrt α] => f

def Cvc.Symbols.Terms.map {Struct : Symbols.Repr} [Syms : Symbols Struct] (terms : Terms) {R : Symbol.Repr} (f : {α : Type} → [inst : IsSrt α] → Symbol.Term α → R α) : Struct R

Equations

• terms.map f = terms.mapM fun {α : Type} [Cvc.IsSrt α] => f

def Cvc.Symbols.Terms.getValues {Struct : Symbols.Repr} [Syms : Symbols Struct] (terms : Terms) : Smt.Sat Values

Retrieves the values of all symbols in a sat context.

Equations

• terms.getValues = terms.mapM fun {α : Type} [Cvc.IsSrt α] => Cvc.Symbol.getValue

def Cvc.Symbols.Terms.getModel {Struct : Symbols.Repr} [Syms : Symbols Struct] (terms : Terms) : Smt.Sat Model

Retrieves the values of all symbols in a sat context.

Equations

• terms.getModel = terms.getValues

def Cvc.Symbols.AliasDsl.Idents.id_Idents : Lean.Ident

Equations

• Cvc.Symbols.AliasDsl.Idents.id_Idents = Lean.mkIdent `Idents

def Cvc.Symbols.AliasDsl.Idents.id_Terms : Lean.Ident

Equations

• Cvc.Symbols.AliasDsl.Idents.id_Terms = Lean.mkIdent `Terms

def Cvc.Symbols.AliasDsl.Idents.id_Model : Lean.Ident

Equations

• Cvc.Symbols.AliasDsl.Idents.id_Model = Lean.mkIdent `Model

def Cvc.Symbols.AliasDsl.Idents.id_FunT : Lean.Ident

Equations

• Cvc.Symbols.AliasDsl.Idents.id_FunT = Lean.mkIdent `FunT

def Cvc.Symbols.AliasDsl.Idents.id_FunctionT : Lean.Ident

Equations

• Cvc.Symbols.AliasDsl.Idents.id_FunctionT = Lean.mkIdent `FunctionT

def Cvc.Symbols.AliasDsl.Idents.id_PredT : Lean.Ident

Equations

• Cvc.Symbols.AliasDsl.Idents.id_PredT = Lean.mkIdent `PredT

def Cvc.Symbols.AliasDsl.Idents.id_PredicateT : Lean.Ident

Equations

• Cvc.Symbols.AliasDsl.Idents.id_PredicateT = Lean.mkIdent `PredicateT

def Cvc.Symbols.AliasDsl.Idents.id_RelT : Lean.Ident

Equations

• Cvc.Symbols.AliasDsl.Idents.id_RelT = Lean.mkIdent `RelT

def Cvc.Symbols.AliasDsl.Idents.id_RelationT : Lean.Ident

Equations

• Cvc.Symbols.AliasDsl.Idents.id_RelationT = Lean.mkIdent `RelationT

def Cvc.Symbols.AliasDsl.Idents.id_Fun : Lean.Ident

Equations

• Cvc.Symbols.AliasDsl.Idents.id_Fun = Lean.mkIdent `Fun

def Cvc.Symbols.AliasDsl.Idents.id_Function : Lean.Ident

Equations

• Cvc.Symbols.AliasDsl.Idents.id_Function = Lean.mkIdent `Function

def Cvc.Symbols.AliasDsl.Idents.id_Pred : Lean.Ident

Equations

• Cvc.Symbols.AliasDsl.Idents.id_Pred = Lean.mkIdent `Pred

def Cvc.Symbols.AliasDsl.Idents.id_Predicate : Lean.Ident

Equations

• Cvc.Symbols.AliasDsl.Idents.id_Predicate = Lean.mkIdent `Predicate

def Cvc.Symbols.AliasDsl.Idents.id_Rel : Lean.Ident

Equations

• Cvc.Symbols.AliasDsl.Idents.id_Rel = Lean.mkIdent `Rel

def Cvc.Symbols.AliasDsl.Idents.id_Relation : Lean.Ident

Equations

• Cvc.Symbols.AliasDsl.Idents.id_Relation = Lean.mkIdent `Relation

def Cvc.Symbols.AliasDsl.Idents.id_monad : Lean.Ident

Equations

• Cvc.Symbols.AliasDsl.Idents.id_monad = Lean.mkIdent `m

def Cvc.Symbols.AliasDsl.Idents.id_α : Lean.Ident

Equations

• Cvc.Symbols.AliasDsl.Idents.id_α = Lean.mkIdent `α

def Cvc.Symbols.AliasDsl.Idents.idRef_Term : Lean.Ident

Equations

• Cvc.Symbols.AliasDsl.Idents.idRef_Term = Lean.mkIdent `Cvc.Term

def Cvc.Symbols.AliasDsl.Idents.idRef_Term_BuildT : Lean.Ident

Equations

• Cvc.Symbols.AliasDsl.Idents.idRef_Term_BuildT = Lean.mkIdent `Cvc.Term.BuildT

def Cvc.Symbols.AliasDsl.Idents.idRef_Symbol : Lean.Ident

Equations

• Cvc.Symbols.AliasDsl.Idents.idRef_Symbol = Lean.mkIdent `Cvc.Symbol

def Cvc.Symbols.AliasDsl.Idents.idRef_Symbol_Repr : Lean.Ident

Equations

• Cvc.Symbols.AliasDsl.Idents.idRef_Symbol_Repr = Lean.mkIdent `Cvc.Symbol.Repr

def Cvc.Symbols.AliasDsl.Idents.idRef_Symbol_mkIdent : Lean.Ident

Equations

• Cvc.Symbols.AliasDsl.Idents.idRef_Symbol_mkIdent = Lean.mkIdent `Cvc.Symbol.mkIdent

def Cvc.Symbols.AliasDsl.Idents.idRef_Symbols : Lean.Ident

Equations

• Cvc.Symbols.AliasDsl.Idents.idRef_Symbols = Lean.mkIdent `Cvc.Symbols

def Cvc.Symbols.AliasDsl.aliasDsl : Lean.ParserDescr

Generates all Cvc.Symbols aliases.

Equations

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

def Cvc.Symbols.AliasDsl.elabAliasDsl : Lean.Elab.Command.CommandElab

Generates all Cvc.Symbols aliases.

Equations

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