Syntax extension for Cvc.Symbols (Cvc.Symbol structures)

TODO

• support extends Sub as long as as a Symbols Sub instance can be found

def Cvc.Symbols.Dsl.symbolTk : Lean.Parser.Parser

Equations

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

def Cvc.Symbols.Dsl.symbolStructure : Lean.Parser.Parser

Equations

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

def Cvc.Symbols.Dsl.symbolStructureSyntax : Lean.ParserDescr

Equations

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

def Cvc.Symbols.Dsl.Idents.id_R : Lean.Ident

Equations

• Cvc.Symbols.Dsl.Idents.id_R = Lean.mkIdent `R

def Cvc.Symbols.Dsl.Idents.id_inst : Lean.Ident

Equations

• Cvc.Symbols.Dsl.Idents.id_inst = Lean.mkIdent `instSymbols

def Cvc.Symbols.Dsl.Idents.id_Spec : Lean.Ident

Equations

• Cvc.Symbols.Dsl.Idents.id_Spec = Lean.mkIdent `Spec

def Cvc.Symbols.Dsl.Idents.id_toSymbols : Lean.Ident

Equations

• Cvc.Symbols.Dsl.Idents.id_toSymbols = Lean.mkIdent `toSymbols

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

Equations

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

def Cvc.Symbols.Dsl.Idents.id_idents : Lean.Ident

Equations

• Cvc.Symbols.Dsl.Idents.id_idents = Lean.mkIdent `idents

def Cvc.Symbols.Dsl.Idents.id_Values : Lean.Ident

Equations

• Cvc.Symbols.Dsl.Idents.id_Values = Lean.mkIdent `Values

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

def Cvc.Symbols.Dsl.Idents.idRef_Repr : Lean.Ident

Equations

• Cvc.Symbols.Dsl.Idents.idRef_Repr = Lean.mkIdent `Cvc.Symbol.Repr

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

Equations

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

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

Equations

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

def Cvc.Symbols.Dsl.elabStateStructureSyntax : Lean.Elab.Command.CommandElab

Equations

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

@[reducible, inline]

abbrev Cvc.Symbols.Dsl.Test.My.Symbols.Fun (α : Type) : Type

Equations

• Cvc.Symbols.Dsl.Test.My.Symbols.Fun = Cvc.Symbols.Fun

@[defaultInstance 1000]

instance Cvc.Symbols.Dsl.Test.My.Symbols.instSymbols : Cvc.Symbols Symbols

Equations

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

@[reducible, inline]

abbrev Cvc.Symbols.Dsl.Test.My.Symbols.Predicate : Type

Equations

• Cvc.Symbols.Dsl.Test.My.Symbols.Predicate = Cvc.Symbols.Dsl.Test.My.Symbols.Pred

@[reducible, inline]

abbrev Cvc.Symbols.Dsl.Test.My.Symbols.Relation : Type

Equations

• Cvc.Symbols.Dsl.Test.My.Symbols.Relation = Cvc.Symbols.Dsl.Test.My.Symbols.Rel

def Cvc.Symbols.Dsl.Test.My.Symbols.myReset! {R✝ : Symbol.Repr} {β✝ : Type} [Symbol.Getter (R✝ Bool) β✝] : Symbols R✝ → β✝

Equations

• self✝.myReset! = Cvc.Symbol.Getter.getInner self✝.myReset

@[reducible, inline]

abbrev Cvc.Symbols.Dsl.Test.My.Symbols.Terms : Type

Equations

• Cvc.Symbols.Dsl.Test.My.Symbols.Terms = Cvc.Symbols.Terms

@[reducible, inline]

abbrev Cvc.Symbols.Dsl.Test.My.Symbols.Values : Type

Equations

• Cvc.Symbols.Dsl.Test.My.Symbols.Values = Cvc.Symbols.Values

@[reducible, inline]

abbrev Cvc.Symbols.Dsl.Test.My.Symbols.idents : Idents

Equations

• Cvc.Symbols.Dsl.Test.My.Symbols.idents = { myCounter := Cvc.Symbol.mkIdent "myCounter", myReset := Cvc.Symbol.mkIdent "myReset" }

@[reducible, inline]

abbrev Cvc.Symbols.Dsl.Test.My.Symbols.Pred : Type

Equations

• Cvc.Symbols.Dsl.Test.My.Symbols.Pred = Cvc.Symbols.Pred

@[reducible, inline]

abbrev Cvc.Symbols.Dsl.Test.My.Symbols.toSymbols : Cvc.Symbols Symbols

Equations

• Cvc.Symbols.Dsl.Test.My.Symbols.toSymbols = Cvc.Symbols.Dsl.Test.My.Symbols.instSymbols

@[reducible, inline]

abbrev Cvc.Symbols.Dsl.Test.My.Symbols.Function (α : Type) : Type

Equations

• Cvc.Symbols.Dsl.Test.My.Symbols.Function = Cvc.Symbols.Function

structure Cvc.Symbols.Dsl.Test.My.Symbols (R : Symbol.Repr) : Type

Testing...

• myCounter : R Int
• myReset : R Bool

@[reducible, inline]

abbrev Cvc.Symbols.Dsl.Test.My.Symbols.Rel : Type

Equations

• Cvc.Symbols.Dsl.Test.My.Symbols.Rel = Cvc.Symbols.Rel

@[reducible, inline]

abbrev Cvc.Symbols.Dsl.Test.My.Symbols.Idents : Type

Equations

• Cvc.Symbols.Dsl.Test.My.Symbols.Idents = Cvc.Symbols.Idents

@[reducible, inline]

abbrev Cvc.Symbols.Dsl.Test.My.Symbols.Model : Type

Equations

• Cvc.Symbols.Dsl.Test.My.Symbols.Model = Cvc.Symbols.Model

@[reducible, inline]

abbrev Cvc.Symbols.Dsl.Test.My.Symbols.Spec : Cvc.Symbols Symbols

Equations

• Cvc.Symbols.Dsl.Test.My.Symbols.Spec = Cvc.Symbols.Dsl.Test.My.Symbols.instSymbols

def Cvc.Symbols.Dsl.Test.My.Symbols.myCounter! {R✝ : Symbol.Repr} {β✝ : Type} [Symbol.Getter (R✝ Int) β✝] : Symbols R✝ → β✝

Equations

• self✝.myCounter! = Cvc.Symbol.Getter.getInner self✝.myCounter

@[reducible, inline]

abbrev Cvc.Symbols.Dsl.Test.MySymbols.Predicate : Type

Equations

• Cvc.Symbols.Dsl.Test.MySymbols.Predicate = Cvc.Symbols.Dsl.Test.MySymbols.Pred

@[reducible, inline]

abbrev Cvc.Symbols.Dsl.Test.MySymbols.Rel : Type

Equations

• Cvc.Symbols.Dsl.Test.MySymbols.Rel = Cvc.Symbols.Rel

@[reducible, inline]

abbrev Cvc.Symbols.Dsl.Test.MySymbols.idents : Idents

Equations

• Cvc.Symbols.Dsl.Test.MySymbols.idents = { myCounter := Cvc.Symbol.mkIdent "myCounter", myReset := Cvc.Symbol.mkIdent "myReset" }

@[reducible, inline]

abbrev Cvc.Symbols.Dsl.Test.MySymbols.Pred : Type

Equations

• Cvc.Symbols.Dsl.Test.MySymbols.Pred = Cvc.Symbols.Pred

@[reducible, inline]

abbrev Cvc.Symbols.Dsl.Test.MySymbols.Fun (α : Type) : Type

Equations

• Cvc.Symbols.Dsl.Test.MySymbols.Fun = Cvc.Symbols.Fun

@[reducible, inline]

abbrev Cvc.Symbols.Dsl.Test.MySymbols.Values : Type

Equations

• Cvc.Symbols.Dsl.Test.MySymbols.Values = Cvc.Symbols.Values

def Cvc.Symbols.Dsl.Test.MySymbols.myReset! {R✝ : Symbol.Repr} {β✝ : Type} [Symbol.Getter (R✝ Bool) β✝] : MySymbols R✝ → β✝

Equations

• self✝.myReset! = Cvc.Symbol.Getter.getInner self✝.myReset

@[reducible, inline]

abbrev Cvc.Symbols.Dsl.Test.MySymbols.toSymbols : Symbols MySymbols

Equations

• Cvc.Symbols.Dsl.Test.MySymbols.toSymbols = Cvc.Symbols.Dsl.Test.MySymbols.instSymbols

@[reducible, inline]

abbrev Cvc.Symbols.Dsl.Test.MySymbols.Spec : Symbols MySymbols

Equations

• Cvc.Symbols.Dsl.Test.MySymbols.Spec = Cvc.Symbols.Dsl.Test.MySymbols.instSymbols

@[reducible, inline]

abbrev Cvc.Symbols.Dsl.Test.MySymbols.Function (α : Type) : Type

Equations

• Cvc.Symbols.Dsl.Test.MySymbols.Function = Cvc.Symbols.Function

@[defaultInstance 1000]

instance Cvc.Symbols.Dsl.Test.MySymbols.instSymbols : Symbols MySymbols

Equations

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

@[reducible, inline]

abbrev Cvc.Symbols.Dsl.Test.MySymbols.Model : Type

Equations

• Cvc.Symbols.Dsl.Test.MySymbols.Model = Cvc.Symbols.Model

@[reducible, inline]

abbrev Cvc.Symbols.Dsl.Test.MySymbols.Relation : Type

Equations

• Cvc.Symbols.Dsl.Test.MySymbols.Relation = Cvc.Symbols.Dsl.Test.MySymbols.Rel

@[reducible, inline]

abbrev Cvc.Symbols.Dsl.Test.MySymbols.Idents : Type

Equations

• Cvc.Symbols.Dsl.Test.MySymbols.Idents = Cvc.Symbols.Idents

def Cvc.Symbols.Dsl.Test.MySymbols.myCounter! {R✝ : Symbol.Repr} {β✝ : Type} [Symbol.Getter (R✝ Int) β✝] : MySymbols R✝ → β✝

Equations

• self✝.myCounter! = Cvc.Symbol.Getter.getInner self✝.myCounter

structure Cvc.Symbols.Dsl.Test.MySymbols (R : Symbol.Repr) : Type

Testing...

• myCounter : R Int
• myReset : R Bool

@[reducible, inline]

abbrev Cvc.Symbols.Dsl.Test.MySymbols.Terms : Type

Equations

• Cvc.Symbols.Dsl.Test.MySymbols.Terms = Cvc.Symbols.Terms