Lean2Js.Text

Imports 1

Init

Decimal numerals and JS / JSON string escaping, for the printers #

The text primitives the printers reach for: decimal numerals and JS / JSON string escaping.

Both are written as recursions over List Char rather than over String, and neither goes through toString. The generated file has to be something a proof can unfold, and Nat.repr and String.foldl are both walls to a proof that wants to read the characters back.

def

Lean2Js.digitChar

source

(d : Nat) :

Char

Equations

Lean2Js.digitChar d = Char.ofNat ('0'.toNat + d)

Instances For

Used by

def

Lean2Js.natDigits

source

@[irreducible]

(n : Nat) :

List Char

The decimal digits, most significant first.

Equations

Lean2Js.natDigits n = if n < 10 then [Lean2Js.digitChar n] else Lean2Js.natDigits (n / 10) ++ [Lean2Js.digitChar (n % 10)]

Instances For

Used by

def

Lean2Js.renderNat

source

(n : Nat) :

String

Equations

Lean2Js.renderNat n = String.ofList (Lean2Js.natDigits n)

Instances For

Used by

def

Lean2Js.renderInt

source

Int → String

Equations

Lean2Js.renderInt (Int.ofNat n) = Lean2Js.renderNat n
Lean2Js.renderInt (Int.negSucc n) = "-" ++ Lean2Js.renderNat (n + 1)

Instances For

Used by

def

Lean2Js.hexDigit

source

(d : Nat) :

Char

Equations

Lean2Js.hexDigit d = if d < 10 then Char.ofNat ('0'.toNat + d) else Char.ofNat ('a'.toNat + d - 10)

Instances For

Used by

def

Lean2Js.hex4

source

(n : Nat) :

String

Equations

Lean2Js.hex4 n = String.ofList [Lean2Js.hexDigit (n / 4096 % 16), Lean2Js.hexDigit (n / 256 % 16), Lean2Js.hexDigit (n / 16 % 16), Lean2Js.hexDigit (n % 16)]

Instances For

Used by

def

Lean2Js.escapeChar

source

(c : Char) :

String

JSON string escaping. It works as is for JS string literals too. U+2028 / U+2029 are not passed through because, legal as they are in JSON, placing them directly in JS source can have them read as line terminators.

Equations