def Cvc.Term.Dsl.smtTerm.quot : Lean.ParserDescr

Equations

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

def Lean.Parser.Category.smtTerm : Category

Equations

• Lean.Parser.Category.smtTerm = { }

def Cvc.Term.Dsl.«smtTerm![_]» : Lean.ParserDescr

Equations

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

def Cvc.Term.Dsl.«smtTerm(_)» : Lean.ParserDescr

Equations

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

def Cvc.Term.Dsl.smtTerm_ : Lean.ParserDescr

Equations

• Cvc.Term.Dsl.smtTerm_ = Lean.ParserDescr.node `Cvc.Term.Dsl.smtTerm_ 1022 (Lean.ParserDescr.const `ident)

def Cvc.Term.Dsl.smtTerm__1 : Lean.ParserDescr

Equations

• Cvc.Term.Dsl.smtTerm__1 = Lean.ParserDescr.node `Cvc.Term.Dsl.smtTerm__1 1022 (Lean.ParserDescr.const `name)

def Cvc.Term.Dsl.smtTerm__2 : Lean.ParserDescr

Equations

• Cvc.Term.Dsl.smtTerm__2 = Lean.ParserDescr.node `Cvc.Term.Dsl.smtTerm__2 1022 (Lean.ParserDescr.const `num)

def Cvc.Term.Dsl.«smtTerm?[_:_]» : Lean.ParserDescr

Equations

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

def Cvc.Term.Dsl.«smtTerm_→_» : Lean.TrailingParserDescr

Equations

• Cvc.Term.Dsl.«smtTerm_→_» = Lean.ParserDescr.trailingNode `Cvc.Term.Dsl.«smtTerm_→_» 25 26 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " → ") (Lean.ParserDescr.cat `smtTerm 25))

def Cvc.Term.Dsl.«smtTerm→[_,_,_,]» : Lean.ParserDescr

Equations

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

def Cvc.Term.Dsl.«smtTerm_∧_» : Lean.TrailingParserDescr

Equations

• Cvc.Term.Dsl.«smtTerm_∧_» = Lean.ParserDescr.trailingNode `Cvc.Term.Dsl.«smtTerm_∧_» 35 36 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ∧ ") (Lean.ParserDescr.cat `smtTerm 35))

def Cvc.Term.Dsl.«smtTerm∧[_,_,_,]» : Lean.ParserDescr

Equations

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

def Cvc.Term.Dsl.«smtTerm_∨_» : Lean.TrailingParserDescr

Equations

• Cvc.Term.Dsl.«smtTerm_∨_» = Lean.ParserDescr.trailingNode `Cvc.Term.Dsl.«smtTerm_∨_» 30 31 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ∨ ") (Lean.ParserDescr.cat `smtTerm 30))

def Cvc.Term.Dsl.«smtTerm∨[_,_,_,]» : Lean.ParserDescr

Equations

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

def Cvc.Term.Dsl.«smtTerm_⊻_» : Lean.TrailingParserDescr

Equations

• Cvc.Term.Dsl.«smtTerm_⊻_» = Lean.ParserDescr.trailingNode `Cvc.Term.Dsl.«smtTerm_⊻_» 30 31 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊻ ") (Lean.ParserDescr.cat `smtTerm 30))

def Cvc.Term.Dsl.«smtTerm⊻[_,_,_,]» : Lean.ParserDescr

Equations

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

def Cvc.Term.Dsl.«smtTerm¬_» : Lean.ParserDescr

Equations

• Cvc.Term.Dsl.«smtTerm¬_» = Lean.ParserDescr.node `Cvc.Term.Dsl.«smtTerm¬_» 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "¬ ") (Lean.ParserDescr.cat `smtTerm 40))

def Cvc.Term.Dsl.smtTermIf__Then__Else__ : Lean.ParserDescr

Equations

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

def Cvc.Term.Dsl.«smtTermLet_←_;__» : Lean.ParserDescr

Equations

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

def Cvc.Term.Dsl.«smtTerm_=_» : Lean.TrailingParserDescr

Equations

• Cvc.Term.Dsl.«smtTerm_=_» = Lean.ParserDescr.trailingNode `Cvc.Term.Dsl.«smtTerm_=_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " = ") (Lean.ParserDescr.cat `smtTerm 50))

def Cvc.Term.Dsl.«smtTerm=[_,_,_,]» : Lean.ParserDescr

Equations

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

def Cvc.Term.Dsl.«smtTerm_≠_» : Lean.TrailingParserDescr

Equations

• Cvc.Term.Dsl.«smtTerm_≠_» = Lean.ParserDescr.trailingNode `Cvc.Term.Dsl.«smtTerm_≠_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≠ ") (Lean.ParserDescr.cat `smtTerm 50))

def Cvc.Term.Dsl.«smtTerm≠[_,_,_,]» : Lean.ParserDescr

Equations

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

def Cvc.Term.Dsl.«smtTerm_≤_» : Lean.TrailingParserDescr

Equations

• Cvc.Term.Dsl.«smtTerm_≤_» = Lean.ParserDescr.trailingNode `Cvc.Term.Dsl.«smtTerm_≤_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≤ ") (Lean.ParserDescr.cat `smtTerm 50))

def Cvc.Term.Dsl.«smtTerm≤[_,_,_,]» : Lean.ParserDescr

Equations

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

def Cvc.Term.Dsl.«smtTerm_≥_» : Lean.TrailingParserDescr

Equations

• Cvc.Term.Dsl.«smtTerm_≥_» = Lean.ParserDescr.trailingNode `Cvc.Term.Dsl.«smtTerm_≥_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≥ ") (Lean.ParserDescr.cat `smtTerm 50))

def Cvc.Term.Dsl.«smtTerm≥[_,_,_,]» : Lean.ParserDescr

Equations

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

def Cvc.Term.Dsl.«smtTerm_<_» : Lean.TrailingParserDescr

Equations

• Cvc.Term.Dsl.«smtTerm_<_» = Lean.ParserDescr.trailingNode `Cvc.Term.Dsl.«smtTerm_<_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " < ") (Lean.ParserDescr.cat `smtTerm 50))

def Cvc.Term.Dsl.«smtTerm<[_,_,_,]» : Lean.ParserDescr

Equations

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

def Cvc.Term.Dsl.«smtTerm_>_» : Lean.TrailingParserDescr

Equations

• Cvc.Term.Dsl.«smtTerm_>_» = Lean.ParserDescr.trailingNode `Cvc.Term.Dsl.«smtTerm_>_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " > ") (Lean.ParserDescr.cat `smtTerm 50))

def Cvc.Term.Dsl.«smtTerm>[_,_,_,]» : Lean.ParserDescr

Equations

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

def Cvc.Term.Dsl.«smtTerm_*_» : Lean.TrailingParserDescr

Equations

• Cvc.Term.Dsl.«smtTerm_*_» = Lean.ParserDescr.trailingNode `Cvc.Term.Dsl.«smtTerm_*_» 70 70 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " * ") (Lean.ParserDescr.cat `smtTerm 71))

def Cvc.Term.Dsl.«smtTerm*[_,_,_,]» : Lean.ParserDescr

Equations

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

def Cvc.Term.Dsl.«smtTerm_/!_» : Lean.TrailingParserDescr

Equations

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

def Cvc.Term.Dsl.«smtTerm/![_,_,_,]» : Lean.ParserDescr

Equations

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

def Cvc.Term.Dsl.«smtTerm_/_» : Lean.TrailingParserDescr

Equations

• Cvc.Term.Dsl.«smtTerm_/_» = Lean.ParserDescr.trailingNode `Cvc.Term.Dsl.«smtTerm_/_» 70 70 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " / ") (Lean.ParserDescr.cat `smtTerm 71))

def Cvc.Term.Dsl.«smtTerm_%_» : Lean.TrailingParserDescr

Equations

• Cvc.Term.Dsl.«smtTerm_%_» = Lean.ParserDescr.trailingNode `Cvc.Term.Dsl.«smtTerm_%_» 70 70 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " % ") (Lean.ParserDescr.cat `smtTerm 71))

def Cvc.Term.Dsl.«smtTerm_+_» : Lean.TrailingParserDescr

Equations

• Cvc.Term.Dsl.«smtTerm_+_» = Lean.ParserDescr.trailingNode `Cvc.Term.Dsl.«smtTerm_+_» 65 65 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " + ") (Lean.ParserDescr.cat `smtTerm 66))

def Cvc.Term.Dsl.«smtTerm+[_,_,_,]» : Lean.ParserDescr

Equations

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

def Cvc.Term.Dsl.«smtTerm_-_» : Lean.TrailingParserDescr

Equations

• Cvc.Term.Dsl.«smtTerm_-_» = Lean.ParserDescr.trailingNode `Cvc.Term.Dsl.«smtTerm_-_» 65 65 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " - ") (Lean.ParserDescr.cat `smtTerm 66))

def Cvc.Term.Dsl.«smtTerm-_» : Lean.ParserDescr

Equations

• Cvc.Term.Dsl.«smtTerm-_» = Lean.ParserDescr.node `Cvc.Term.Dsl.«smtTerm-_» 75 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "- ") (Lean.ParserDescr.cat `smtTerm 0))

def Cvc.Term.Dsl.smtTerm___ : Lean.TrailingParserDescr

Equations

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

def Cvc.Term.Dsl.termSmt!___ : Lean.ParserDescr

Equations

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

def Cvc.Term.Dsl.«termSmt!FunSmtFun!___=>___» : Lean.ParserDescr

Equations

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

def Cvc.Term.Dsl.«termSmtPred!SmtPredicate!___=>___» : Lean.ParserDescr

Equations

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

def Cvc.Term.Dsl.«termSmtRel!SmtRelation!_____=>___» : Lean.ParserDescr

Equations

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