HandleNumOrIdent

This module provides elaboration helpers for numeric/identifier operands.

def mkUIntOfNat (n : Nat) : Lean.Expr

Build the Expr UInt64.ofNat n from a Nat.

Equations

• mkUIntOfNat n = (Lean.Expr.const `UInt64.ofNat []).app (Lean.mkNatLit n)

def mkUintOfNat (n : UInt64) : Lean.Expr

Build the Expr of the numeral denoting the UInt64 n.

Equations

• mkUintOfNat n = (Lean.Expr.const `OfNat.ofNat []).app (Lean.mkNatLit n.toNat)

def mkUInt64Lit (n : UInt64) : Lean.Expr

Build the Expr of the UInt64 literal n.

Equations

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

def parseMriscxNumOrIdentToTerm (s : Lean.Syntax) : Lean.Elab.TermElabM Lean.Term

Elaborate a num-or-ident syntax node into the term it denotes.

Equations

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

def parseTermToMriscxNumOrIdent (s : Lean.TSyntax `term) : Lean.TSyntax `mriscxNumOrIdent

Reinterpret a term as mriscxNumOrIdent syntax.

Equations

• parseTermToMriscxNumOrIdent s = { raw := s.raw }

def parseMriscxNumOrIdent (s : Lean.Syntax) : Lean.Elab.TermElabM Lean.Expr

A function that first checks whether the given num or ident is a numeric literal. If so, it returns the corresponding UInt64 expression. If not, it checks if the variable name has been declared as a UInt64 in the current context and, if found, returns it as an expression. If neither condition is met, the function fails. To be able to check if the variable has already been declared, the MetaM Monad is required. For this reason, we return a TermElabM Expr, which has to be lifted afterwards.

Equations

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

def parseMriscxNumOrIdentArray (a : Array Lean.Syntax) : Lean.Elab.TermElabM (Array Lean.Expr)

Apply parseMriscxNumOrIdent on all elements inside an array

Equations

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

def parseLabelname (s : Lean.TSyntax `ident) (withDot : Bool) : Lean.Elab.TermElabM Lean.Expr

Elaborate a label identifier into its string Expr, honouring the leading-dot form.

Equations

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

def checkIfVariableToTerm (t : Lean.TSyntax `ident) (identWithDot : Bool) : Lean.Elab.TermElabM Lean.Term

Turn a label identifier into the term naming its target, honouring the leading-dot form.

Equations

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

def numOrIdentToSyntax (t : Lean.TSyntax `term) : Lean.PrettyPrinter.UnexpandM (Lean.TSyntax `mriscxNumOrIdent)

Unexpand a term back into mriscxNumOrIdent surface syntax.

Equations

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