def Auto.Lexer.SMT.whitespace : String

Equations

• Auto.Lexer.SMT.whitespace = { data := List.map Char.ofNat [9, 10, 13, 32] }

def Auto.Lexer.SMT.unprintable : String

Equations

• Auto.Lexer.SMT.unprintable = { data := List.map Char.ofNat (127 :: List.range 32) }

def Auto.Lexer.SMT.comment : Regex.ERE

Equations

• Auto.Lexer.SMT.comment = Auto.Regex.ERE.comp #[Auto.Regex.ERE.ofStr ";", (Auto.Regex.ERE.bracketN (Auto.Regex.EREBracket.inStr "\n")).star, Auto.Regex.ERE.ofStr "\n"]

def Auto.Lexer.SMT.numeral : Regex.ERE

Equations

• Auto.Lexer.SMT.numeral = Auto.Regex.ERE.plus #[Auto.Regex.ERE.ofStr "0", Auto.Regex.ERE.comp #[Auto.Regex.ERE.inStr "123456789", (Auto.Regex.ERE.ofCC Auto.Regex.CC.Ty.digit).star]]

def Auto.Lexer.SMT.decimal : Regex.ERE

Equations

• Auto.Lexer.SMT.decimal = Auto.Regex.ERE.comp #[Auto.Lexer.SMT.numeral, Auto.Regex.ERE.inStr ".", (Auto.Regex.ERE.ofCC Auto.Regex.CC.Ty.digit).some]

def Auto.Lexer.SMT.hexadecimal : Regex.ERE

Equations

• Auto.Lexer.SMT.hexadecimal = Auto.Regex.ERE.comp #[Auto.Regex.ERE.ofStr "#x", (Auto.Regex.ERE.ofCC Auto.Regex.CC.Ty.xdigit).some]

def Auto.Lexer.SMT.binary : Regex.ERE

Equations

• Auto.Lexer.SMT.binary = Auto.Regex.ERE.comp #[Auto.Regex.ERE.ofStr "#b", (Auto.Regex.ERE.inStr "01").some]

def Auto.Lexer.SMT.string : Regex.ERE

Equations

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

def Auto.Lexer.SMT.simpleSymbol : Regex.ERE

Equations

• Auto.Lexer.SMT.simpleSymbol = Auto.Regex.ERE.comp #[Auto.Regex.ERE.bracket Auto.Lexer.SMT.ssymbstart✝, (Auto.Regex.ERE.bracket Auto.Lexer.SMT.ssymbchars✝).star]

def Auto.Lexer.SMT.quotedSymbol : Regex.ERE

Equations

• Auto.Lexer.SMT.quotedSymbol = Auto.Regex.ERE.comp #[Auto.Regex.ERE.inStr "|", (Auto.Regex.ERE.bracketN Auto.Lexer.SMT.notqsymbchars✝).star, Auto.Regex.ERE.inStr "|"]

def Auto.Lexer.SMT.symbol : Regex.ERE

Equations

• Auto.Lexer.SMT.symbol = Auto.Regex.ERE.plus #[Auto.Lexer.SMT.simpleSymbol.attr "simplesymbol", Auto.Lexer.SMT.quotedSymbol.attr "quotedsymbol"]

def Auto.Lexer.SMT.keyword : Regex.ERE

Equations

• Auto.Lexer.SMT.keyword = Auto.Regex.ERE.comp #[Auto.Regex.ERE.inStr ":", Auto.Lexer.SMT.simpleSymbol]

def Auto.Lexer.SMT.lparen : Regex.ERE

Equations

• Auto.Lexer.SMT.lparen = Auto.Regex.ERE.inStr "("

def Auto.Lexer.SMT.rparen : Regex.ERE

Equations

• Auto.Lexer.SMT.rparen = Auto.Regex.ERE.inStr ")"

def Auto.Lexer.SMT.underscore : Regex.ERE

Equations

• Auto.Lexer.SMT.underscore = Auto.Regex.ERE.ofStr "_"

def Auto.Lexer.SMT.SMTforall : Regex.ERE

Equations

• Auto.Lexer.SMT.SMTforall = Auto.Regex.ERE.ofStr "forall"

def Auto.Lexer.SMT.SMTexists : Regex.ERE

Equations

• Auto.Lexer.SMT.SMTexists = Auto.Regex.ERE.ofStr "exists"

def Auto.Lexer.SMT.SMTlambda : Regex.ERE

Equations

• Auto.Lexer.SMT.SMTlambda = Auto.Regex.ERE.ofStr "lambda"

def Auto.Lexer.SMT.SMTlet : Regex.ERE

Equations

• Auto.Lexer.SMT.SMTlet = Auto.Regex.ERE.ofStr "let"

def Auto.Lexer.SMT.specConst : Regex.ERE

Special constants

Equations

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

def Auto.Lexer.SMT.sexpr : Regex.ERE

Equations

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

def Auto.Lexer.SMT.index : Regex.ERE

Equations

• Auto.Lexer.SMT.index = Auto.Regex.ERE.plus #[Auto.Lexer.SMT.numeral.attr "numeral", Auto.Lexer.SMT.symbol]

def Auto.Lexer.SMT.identifier : Regex.ERE

Equations

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

def Auto.Lexer.SMT.sort : Regex.ERE

Equations

• Auto.Lexer.SMT.sort = Auto.Regex.ERE.plus #[Auto.Lexer.SMT.identifier, Auto.Lexer.SMT.lparen.attr "(", Auto.Lexer.SMT.rparen.attr ")"]

def Auto.Lexer.SMT.sorted_var : Regex.ERE

Equations

• Auto.Lexer.SMT.sorted_var = Auto.Regex.ERE.plus #[Auto.Lexer.SMT.symbol, Auto.Lexer.SMT.lparen.attr "(", Auto.Lexer.SMT.rparen.attr ")", Auto.Lexer.SMT.sort]

def Auto.Lexer.SMT.term : Regex.ERE

Equations

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

def Auto.Lexer.SMT.instHashableChar_auto : Hashable Char

Equations

• Auto.Lexer.SMT.instHashableChar_auto = { hash := fun (c : Char) => hash c.val }

opaque Auto.Lexer.SMT.lexiconADFA : Regex.ADFA Char