DSL for definition DRY

def cvc5.externKw.quot : Lean.ParserDescr

Equations

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

def Lean.Parser.Category.externKw : Category

Equations

• Lean.Parser.Category.externKw = { }

def cvc5.defsItem.quot : Lean.ParserDescr

Equations

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

def Lean.Parser.Category.defsItem : Category

Equations

• Lean.Parser.Category.defsItem = { }

def Lean.Parser.Category.defsItemHead : Category

Equations

• Lean.Parser.Category.defsItemHead = { }

def cvc5.defsItemHead.quot : Lean.ParserDescr

Equations

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

def Lean.Parser.Category.defsItemTail!? : Category

Equations

• Lean.Parser.Category.defsItemTail!? = { }

def cvc5.defsItemTail!?.quot : Lean.ParserDescr

Equations

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

def Lean.Parser.Category.defsItemTail : Category

Equations

• Lean.Parser.Category.defsItemTail = { }

def cvc5.defsItemTail.quot : Lean.ParserDescr

Equations

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

def cvc5.defsMod.quot : Lean.ParserDescr

Equations

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

def Lean.Parser.Category.defsMod : Category

Equations

• Lean.Parser.Category.defsMod = { }

def cvc5.forallArity : Lean.Expr → Nat

Arity of an expression.

Stolen from batteries.

Equations

• cvc5.forallArity (Lean.Expr.mdata data b) = cvc5.forallArity b
• cvc5.forallArity (Lean.Expr.forallE binderName binderType body binderInfo) = 1 + cvc5.forallArity body
• cvc5.forallArity x✝ = 0

def cvc5.defsMod? : Lean.ParserDescr

Equations

• cvc5.defsMod? = Lean.ParserDescr.node `cvc5.defsMod? 1024 (Lean.ParserDescr.symbol "?")

def cvc5.defsMod! : Lean.ParserDescr

Equations

• cvc5.defsMod! = Lean.ParserDescr.node `cvc5.defsMod! 1024 (Lean.ParserDescr.symbol "!")

def cvc5.defsMod!? : Lean.ParserDescr

Equations

• cvc5.defsMod!? = Lean.ParserDescr.node `cvc5.defsMod!? 1024 (Lean.ParserDescr.symbol "!?")

def cvc5.defsMod?! : Lean.ParserDescr

Equations

• cvc5.defsMod?! = Lean.ParserDescr.node `cvc5.defsMod?! 1024 (Lean.ParserDescr.symbol "?!")

def cvc5.defsItemStxHead : Lean.ParserDescr

Equations

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

def cvc5.defsItemStxTail!? : Lean.ParserDescr

Equations

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

def cvc5.defsItemStxTail : Lean.ParserDescr

Equations

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

def cvc5.defsItemStx : Lean.ParserDescr

Equations

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

unsafe def cvc5.elabDefsItem (pref : String) (forceMods : Option (Lean.TSyntax `defsMod)) : Lean.Elab.Command.CommandElab

Equations

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

def cvc5.multidefs : Lean.ParserDescr

Defines similar functions realized by extern.

extern! in "prefix"
  /-- Create a Boolean constant.

  - `b`: The Boolean constant.

  Will create an opaque definition with `[@extern extStr]` where
  `extStr = "prefix" ++ "_" ++ "myFunction"`.
  -/
  def myFunction : Term → Except Error Op
  with!?
    endsWithBang!
    endWithQuestion?
  with
    myOtherFunction : Term → Op :=
      Error.unwrap! ∘ myFunction
    /-- Optional function docstring: if none, inherit from the main function. -/
    yetAnotherFunction : Term → Option Op :=
      Except.toOption ∘ myFunction

• in "prefix" is optional; if none, then the prefix will be the (last component of the) name of the current namespace with the first letter lowercased. Fails if the current namespace has no components.

• with ...: takes a sequence of identifiers, each generate a function that

  • unwraps the result if !-ended, which generates code similar to myOtherFunction above;
  • turns a result into an option if ?-ended, which generates code similar to yetAnotherFunction above;
  • fails otherwise.

  The with ... syntax is currently only compatible with external functions that produce Except Error α values.

• Supports declModifiers on the main (def) function myFunction such as private.

• Accepts a list of external (def) functions, each with its with clauses.

This macro can generate optional (?) and panic (!) wrappers even more automatically.

extern! "prefix"
  /-- Create a Boolean constant.

  - `b`: The Boolean constant.

  Will create an opaque definition with `[@extern extStr]` where
  `extStr = "prefix" ++ "_" ++ "myFunction"`.
  -/
  def !? myFunction : Term → Except Error Op
  with
    myOtherFunction : Term → Op :=
      myFunction!
    /-- Optional function docstring: if none, inherit from the main function. -/
    yetAnotherFunction : Term → Option Op :=
      myFunction?

Notice the !? between def and myFunction. This generates myFunction! and myFunction? which respectively panic-unwrap errors and turn the Except into an Option. In other words, it is the same as (and internally turned into) a with!? myFunction! myFunction? clause using the first syntax above.

Besides !?, the following are also supported:

• ?!: same behavior as !?;
• !: only generate the panic unwrapper;
• ?: only generate the Option unwrapper.

Equations

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

unsafe def cvc5.multidefsImpl : Lean.Elab.Command.CommandElab

Defines similar functions realized by extern.

extern! in "prefix"
  /-- Create a Boolean constant.

  - `b`: The Boolean constant.

  Will create an opaque definition with `[@extern extStr]` where
  `extStr = "prefix" ++ "_" ++ "myFunction"`.
  -/
  def myFunction : Term → Except Error Op
  with!?
    endsWithBang!
    endWithQuestion?
  with
    myOtherFunction : Term → Op :=
      Error.unwrap! ∘ myFunction
    /-- Optional function docstring: if none, inherit from the main function. -/
    yetAnotherFunction : Term → Option Op :=
      Except.toOption ∘ myFunction

• in "prefix" is optional; if none, then the prefix will be the (last component of the) name of the current namespace with the first letter lowercased. Fails if the current namespace has no components.

• with ...: takes a sequence of identifiers, each generate a function that

  • unwraps the result if !-ended, which generates code similar to myOtherFunction above;
  • turns a result into an option if ?-ended, which generates code similar to yetAnotherFunction above;
  • fails otherwise.

  The with ... syntax is currently only compatible with external functions that produce Except Error α values.

• Supports declModifiers on the main (def) function myFunction such as private.

• Accepts a list of external (def) functions, each with its with clauses.

This macro can generate optional (?) and panic (!) wrappers even more automatically.

extern! "prefix"
  /-- Create a Boolean constant.

  - `b`: The Boolean constant.

  Will create an opaque definition with `[@extern extStr]` where
  `extStr = "prefix" ++ "_" ++ "myFunction"`.
  -/
  def !? myFunction : Term → Except Error Op
  with
    myOtherFunction : Term → Op :=
      myFunction!
    /-- Optional function docstring: if none, inherit from the main function. -/
    yetAnotherFunction : Term → Option Op :=
      myFunction?

Notice the !? between def and myFunction. This generates myFunction! and myFunction? which respectively panic-unwrap errors and turn the Except into an Option. In other words, it is the same as (and internally turned into) a with!? myFunction! myFunction? clause using the first syntax above.

Besides !?, the following are also supported:

• ?!: same behavior as !?;
• !: only generate the panic unwrapper;
• ?: only generate the Option unwrapper.

Equations

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

def cvc5.externkw : Lean.ParserDescr

Equations

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

def cvc5.externdef : Lean.ParserDescr

Defines an external, opaque function with optional helpers.

/-- Some documentation. -/
extern_def!? in "prefix" myFunction : Term → Except Error Op

Generates an opaque definition

/-- Some documentation. -/
@[extern "prefix_myFunction"]
def myFunction : Term → Except Error Op

• in "prefix" is optional, uses the current namespace with first letter lowercased if none.

• extern_def!? also defines myFunction! : Term → Op and myFunction? : Term → Option Op in terms of myFunction.

  Other variants exist:

  • extern_def?!: same as extern_def!?;
  • extern_def?: only defines myFunction?;
  • extern_def!: only defines myFunction!;
  • extern_def: defines nothing besides myFunction.

Equations

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

unsafe def cvc5.externdefImpl : Lean.Elab.Command.CommandElab

Defines an external, opaque function with optional helpers.

/-- Some documentation. -/
extern_def!? in "prefix" myFunction : Term → Except Error Op

Generates an opaque definition

/-- Some documentation. -/
@[extern "prefix_myFunction"]
def myFunction : Term → Except Error Op

• in "prefix" is optional, uses the current namespace with first letter lowercased if none.

• extern_def!? also defines myFunction! : Term → Op and myFunction? : Term → Option Op in terms of myFunction.

  Other variants exist:

  • extern_def?!: same as extern_def!?;
  • extern_def?: only defines myFunction?;
  • extern_def!: only defines myFunction!;
  • extern_def: defines nothing besides myFunction.

Equations

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