DSL for definition DRY

def cvc5.Init.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.Init.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 cvc5.Init.defsItemHead.quot : Lean.ParserDescr

Equations

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

def Lean.Parser.Category.defsItemHead : Category

Equations

• Lean.Parser.Category.defsItemHead = { }

def cvc5.Init.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.Init.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 Lean.Parser.Category.defsMod : Category

Equations

• Lean.Parser.Category.defsMod = { }

def cvc5.Init.defsMod.quot : Lean.ParserDescr

Equations

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

def cvc5.Init.defsMod? : Lean.ParserDescr

Equations

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

def cvc5.Init.defsMod! : Lean.ParserDescr

Equations

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

def cvc5.Init.defsMod!? : Lean.ParserDescr

Equations

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

def cvc5.Init.defsMod?! : Lean.ParserDescr

Equations

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

def cvc5.Init.defsItemStxHead : Lean.ParserDescr

Equations

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

def cvc5.Init.defsItemStxTail!? : Lean.ParserDescr

Equations

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

def cvc5.Init.defsItemStxTail : Lean.ParserDescr

Equations

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

def cvc5.Init.defsItemStx : Lean.ParserDescr

Equations

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

def cvc5.Init.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.Init.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.Init.externkw : Lean.ParserDescr

Equations

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

def cvc5.Init.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.Init.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.