Declare type aliases of Ordinal

This repository contains two type aliases of Ordinal, each preserving the order structure but with distinct arithmetic defined on it, namely NatOrdinal and Nimber. We define a ordinal_alias! macro which contains all the boilerplate required to set up these types. This also ensures that the API between both stays consistent.

def mkDocComment (s : String) : Lean.TSyntax `Lean.Parser.Command.docComment

Doc-comment allowing antiquotation.

Equations

• mkDocComment s = { raw := (Lean.mkNode `Lean.Parser.Command.docComment #[Lean.mkAtom "/--", Lean.mkAtom (s ++ "-/")]).raw }

def mkOf (Alias : Lean.TSyntax `ident) : Lean.TSyntax `ident

Alias.of

Equations

• mkOf Alias = { raw := (Lean.mkIdent (Alias.getId ++ `of)).raw }

def mkVal (Alias : Lean.TSyntax `ident) : Lean.TSyntax `ident

Alias.val

Equations

• mkVal Alias = { raw := (Lean.mkIdent (Alias.getId ++ `val)).raw }

def commandOrdinal_alias!__ : Lean.ParserDescr

Declare a type alias of Ordinal, preserving the order structure.

Equations

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