Skip to content

Lean2Js.Parse

Imports 4

A reader for the text the printers write #

A reader for the text the printers write, and the proof that it gives the printers' input back.

The grammar it accepts is not JavaScript: it is the subset this compiler emits, which is fully parenthesised and has no optional whitespace. Reading JS is not the goal — reading back what was written is.

Every reader takes a List Char and returns what it read together with the characters left over, so the roundtrip lemmas compose: each one is stated about a rendering followed by an arbitrary remainder.

Decimal numerals #

def

Lean2Js.Parse.digitVal

(c : Char) :

Equations

Lean2Js.Parse.digitVal c = c.toNat - '0'.toNat

Instances For

Used by

def

Lean2Js.Parse.parseDigits

(acc : Nat) :

List Char → Nat × List Char

Equations

Lean2Js.Parse.parseDigits acc [] = (acc, [])
Lean2Js.Parse.parseDigits acc (c :: rest) = if c.isDigit = true then Lean2Js.Parse.parseDigits (acc * 10 + Lean2Js.Parse.digitVal c) rest else (acc, c :: rest)

Instances For

Used by

def

Lean2Js.Parse.parseNat

:

List Char → Option (Nat × List Char)

Equations

Lean2Js.Parse.parseNat [] = none
Lean2Js.Parse.parseNat (c :: rest) = if c.isDigit = true then some (Lean2Js.Parse.parseDigits (Lean2Js.Parse.digitVal c) rest) else none

Instances For

Used by

def

Lean2Js.Parse.parseInt

(cs : List Char) :

Option (Int × List Char)

Equations

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

Instances For

Used by

def

Lean2Js.Parse.notDigitFirst

(cs : List Char) :

What a numeral can be followed by. A reader of digits is greedy, so the character after the numeral has to be one it will not take.

Equations

Lean2Js.Parse.notDigitFirst cs = ∀ (c : Char) (rest : List Char), cs = c :: rest → c.isDigit = false

Instances For

Used by

theorem

Lean2Js.Parse.digitVal_digitChar

{d : Nat} (h : d < 10) :

digitVal (digitChar d) = d

Used by

theorem

Lean2Js.Parse.isDigit_digitChar

{d : Nat} (h : d < 10) :

(digitChar d).isDigit = true

Used by

theorem

Lean2Js.Parse.natDigits_all_digit

(n : Nat) :

(natDigits n).all Char.isDigit = true

Used by

theorem

Lean2Js.Parse.natDigits_ne_nil

(n : Nat) :

natDigits n ≠ []

Used by

theorem

Lean2Js.Parse.parseDigits_append

(ds : List Char) (hds : ds.all Char.isDigit = true) (rest : List Char) (hrest : notDigitFirst rest) (acc : Nat) :

parseDigits acc (ds ++ rest) = (List.foldl (fun (a : Nat) (c : Char) => a * 10 + digitVal c) acc ds, rest)

Reading digits off a rendering of n, with anything that is not a digit behind it, gives n back and leaves the remainder untouched.

Used by

theorem

Lean2Js.Parse.foldl_natDigits

(n : Nat) :

List.foldl (fun (a : Nat) (c : Char) => a * 10 + digitVal c) 0 (natDigits n) = n

Used by

theorem

Lean2Js.Parse.toList_renderNat

(n : Nat) :

(renderNat n).toList = natDigits n

Used by

theorem

Lean2Js.Parse.parseNat_append

(n : Nat) (rest : List Char) (hrest : notDigitFirst rest) :

parseNat ((renderNat n).toList ++ rest) = some (n, rest)

Used by

theorem

Lean2Js.Parse.head_natDigits_ne_neg

{n : Nat} {d : Char} {ds : List Char} (hn : natDigits n = d :: ds) :

d ≠ '-'

Used by

theorem

Lean2Js.Parse.parseInt_ofNat

(n : Nat) (rest : List Char) (hrest : notDigitFirst rest) :

parseInt ((renderNat n).toList ++ rest) = some (↑n, rest)

Used by

theorem

Lean2Js.Parse.parseInt_negSucc

(n : Nat) (rest : List Char) (hrest : notDigitFirst rest) :

parseInt ('-' :: (renderNat (n + 1)).toList ++ rest) = some (Int.negSucc n, rest)

Used by

theorem

Lean2Js.Parse.parseInt_append

(i : Int) (rest : List Char) (hrest : notDigitFirst rest) :

parseInt ((renderInt i).toList ++ rest) = some (i, rest)

Used by

String literals #

def

Lean2Js.Parse.hexVal

(c : Char) :

Equations

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

Instances For

Used by

def

Lean2Js.Parse.unescape

:

List Char → Option (List Char × List Char)

Reads the body of a string literal up to its closing quote, returning the characters it stood for and what follows the quote.

Equations

One or more equations did not get rendered due to their size.
Lean2Js.Parse.unescape [] = none
Lean2Js.Parse.unescape ('\"' :: rest) = some ([], rest)
Lean2Js.Parse.unescape ('\\' :: 'n' :: rest) = Option.map (fun (p : List Char × List Char) => ('\n' :: p.fst, p.snd)) (Lean2Js.Parse.unescape rest)
Lean2Js.Parse.unescape ('\\' :: 'r' :: rest) = Option.map (fun (p : List Char × List Char) => ('\x0d' :: p.fst, p.snd)) (Lean2Js.Parse.unescape rest)
Lean2Js.Parse.unescape ('\\' :: 't' :: rest) = Option.map (fun (p : List Char × List Char) => ('\t' :: p.fst, p.snd)) (Lean2Js.Parse.unescape rest)
Lean2Js.Parse.unescape ('\\' :: '\"' :: rest) = Option.map (fun (p : List Char × List Char) => ('\"' :: p.fst, p.snd)) (Lean2Js.Parse.unescape rest)
Lean2Js.Parse.unescape ('\\' :: '\\' :: rest) = Option.map (fun (p : List Char × List Char) => ('\\' :: p.fst, p.snd)) (Lean2Js.Parse.unescape rest)
Lean2Js.Parse.unescape ('\\' :: tail) = none
Lean2Js.Parse.unescape (c :: rest) = Option.map (fun (p : List Char × List Char) => (c :: p.fst, p.snd)) (Lean2Js.Parse.unescape rest)

Instances For

Used by

def

Lean2Js.Parse.parseStr

:

List Char → Option (String × List Char)

Equations

Lean2Js.Parse.parseStr ('\"' :: rest) = Option.map (fun (p : List Char × List Char) => (String.ofList p.fst, p.snd)) (Lean2Js.Parse.unescape rest)
Lean2Js.Parse.parseStr x✝ = none

Instances For

Used by

theorem

Lean2Js.Parse.hex4_toList

(n : Nat) :

(hex4 n).toList = [hexDigit (n / 4096 % 16), hexDigit (n / 256 % 16), hexDigit (n / 16 % 16), hexDigit (n % 16)]

Used by

theorem

Lean2Js.Parse.hexVal_hexDigit

{d : Nat} (h : d < 16) :

hexVal (hexDigit d) = some d

Used by

theorem

Lean2Js.Parse.unescape_hex4

(n : Nat) (h : n < 65536) (tail : List Char) :

unescape ('\\' :: 'u' :: ((hex4 n).toList ++ tail)) = Option.map (fun (p : List Char × List Char) => (Char.ofNat n :: p.fst, p.snd)) (unescape tail)

Used by

theorem

Lean2Js.Parse.unescape_plain

{c : Char} (h1 : c ≠ '\"') (h2 : c ≠ '\\') (tail : List Char) :

unescape (c :: tail) = Option.map (fun (p : List Char × List Char) => (c :: p.fst, p.snd)) (unescape tail)

Used by

theorem

Lean2Js.Parse.unescape_escapeChar

(c : Char) (tail : List Char) :

unescape ((escapeChar c).toList ++ tail) = Option.map (fun (p : List Char × List Char) => (c :: p.fst, p.snd)) (unescape tail)

Used by

theorem

Lean2Js.Parse.unescape_escapeChars

(cs tail : List Char) :

unescape ((escapeChars cs).toList ++ '\"' :: tail) = some (cs, tail)

Used by

theorem

Lean2Js.Parse.parseStr_append

(s : String) (tail : List Char) :

parseStr (("\"" ++ escapeString s ++ "\"").toList ++ tail) = some (s, tail)

Used by

theorem

Lean2Js.Parse.parseStr_cons

(s : String) (tail : List Char) :

parseStr ('\"' :: ((escapeString s).toList ++ '\"' :: tail)) = some (s, tail)

The shape a string literal takes inside a larger rendering, where the quotes are part of a neighbouring chunk of literal text rather than of the escaped body.

Used by

theorem

Lean2Js.Parse.parseStr_ctors

(tail : List Char) :

parseStr ('\"' :: 'c' :: 't' :: 'o' :: 'r' :: 's' :: '\"' :: tail) = some ("ctors", tail)

The head of a descriptor for a declared type, read back while parseStr stays folded: the key that follows it is a string the author chose, and reading that one needs parseStr_cons.

Used by

theorem

Lean2Js.Parse.parseStr_mu

(tail : List Char) :

parseStr ('\"' :: 'm' :: 'u' :: '\"' :: tail) = some ("mu", tail)

Used by

theorem

Lean2Js.Parse.parseStr_ref

(tail : List Char) :

parseStr ('\"' :: 'r' :: 'e' :: 'f' :: '\"' :: tail) = some ("ref", tail)

Used by

Identifiers #

def

Lean2Js.Parse.parseIdentChars

:

List Char → List Char × List Char

Equations

Lean2Js.Parse.parseIdentChars [] = ([], [])
Lean2Js.Parse.parseIdentChars (c :: rest) = if Lean2Js.isIdentPart c = true then match Lean2Js.Parse.parseIdentChars rest with | (ds, r) => (c :: ds, r) else ([], c :: rest)

Instances For

Used by

def

Lean2Js.Parse.parseIdent

(cs : List Char) :

Option (String × List Char)

Equations

Lean2Js.Parse.parseIdent cs = match Lean2Js.Parse.parseIdentChars cs with | (ds, r) => if ds.isEmpty = true then none else some (String.ofList ds, r)

Instances For

Used by

def

Lean2Js.Parse.notIdentFirst

(cs : List Char) :

What a name can be followed by. A reader of names is greedy, so the character after the name has to be one it will not take.

Equations

Lean2Js.Parse.notIdentFirst cs = ∀ (c : Char) (rest : List Char), cs = c :: rest → Lean2Js.isIdentPart c = false

Instances For

Used by

theorem

Lean2Js.Parse.parseIdentChars_append

(ds : List Char) (hds : ds.all isIdentPart = true) (rest : List Char) (hrest : notIdentFirst rest) :

parseIdentChars (ds ++ rest) = (ds, rest)

Used by

theorem

Lean2Js.Parse.parseIdent_append

(name : String) (hne : name.toList ≠ []) (hall : name.toList.all isIdentPart = true) (rest : List Char) (hrest : notIdentFirst rest) :

parseIdent (name.toList ++ rest) = some (name, rest)

Used by

Literal chunks #

def

Lean2Js.Parse.expect

:

List Char → List Char → Option (List Char)

Equations

Lean2Js.Parse.expect [] x✝ = some x✝
Lean2Js.Parse.expect (l :: ls) (c :: cs) = if l = c then Lean2Js.Parse.expect ls cs else none
Lean2Js.Parse.expect (head :: tail) [] = none

Instances For

Used by

theorem

Lean2Js.Parse.expect_append

(lit rest : List Char) :

expect lit (lit ++ rest) = some rest

Used by

Type descriptors #

The budget is the descriptor's own size, which the caller reads off the text it is about to hand over. It bounds the descent, not the guarantee: the roundtrip below holds for every budget that is large enough, and the top-level reader takes the length of the text it was given.

def

Lean2Js.Parse.descSize

@[irreducible]

:

Js.TyDesc → Nat

Equations

Instances For

Used by

def

Lean2Js.Parse.altsSize

@[irreducible]

:

List (String × List (String × Js.TyDesc)) → Nat

Equations

Lean2Js.Parse.altsSize [] = 1
Lean2Js.Parse.altsSize ((fst, fs) :: rest) = Lean2Js.Parse.fieldsSize fs + Lean2Js.Parse.altsSize rest + 1

Instances For

Used by

def

Lean2Js.Parse.fieldsSize

@[irreducible]

:

List (String × Js.TyDesc) → Nat

Equations

Lean2Js.Parse.fieldsSize [] = 1
Lean2Js.Parse.fieldsSize ((fst, d) :: rest) = Lean2Js.Parse.descSize d + Lean2Js.Parse.fieldsSize rest + 1

Instances For

Used by

def

Lean2Js.Parse.parseDesc

:

Nat → List Char → Option (Js.TyDesc × List Char)

Equations

One or more equations did not get rendered due to their size.
Lean2Js.Parse.parseDesc 0 x✝ = none

Instances For

Used by

def

Lean2Js.Parse.parseAlts

:

Nat → List Char → Option (List (String × List (String × Js.TyDesc)) × List Char)

Equations

One or more equations did not get rendered due to their size.
Lean2Js.Parse.parseAlts 0 x✝ = none
Lean2Js.Parse.parseAlts f.succ (']' :: tail) = some ([], ']' :: tail)

Instances For

Used by

def

Lean2Js.Parse.parseFields

:

Nat → List Char → Option (List (String × Js.TyDesc) × List Char)

Equations

One or more equations did not get rendered due to their size.
Lean2Js.Parse.parseFields 0 x✝ = none
Lean2Js.Parse.parseFields f.succ (']' :: tail) = some ([], ']' :: tail)

Instances For

Used by

theorem

Lean2Js.Parse.descSize_pos

(d : Js.TyDesc) :

Used by

theorem

Lean2Js.Parse.altsSize_pos

(alts : List (String × List (String × Js.TyDesc))) :

0 < altsSize alts

Used by

theorem

Lean2Js.Parse.fieldsSize_pos

(fs : List (String × Js.TyDesc)) :

0 < fieldsSize fs

Used by

theorem

Lean2Js.Parse.parseDesc_append

(d : Js.TyDesc) (f : Nat) (hf : descSize d ≤ f) (rest : List Char) :

parseDesc f (d.render.toList ++ rest) = some (d, rest)

Used by

theorem

Lean2Js.Parse.parseAlts_append

(alts : List (String × List (String × Js.TyDesc))) (f : Nat) (hf : altsSize alts ≤ f) (rest : List Char) (hrest : ∃ (r : List Char), rest = ']' :: r) :

parseAlts f ((Js.TyDesc.renderAlts alts).toList ++ rest) = some (alts, rest)

Used by

theorem

Lean2Js.Parse.parseFields_append

(fs : List (String × Js.TyDesc)) (f : Nat) (hf : fieldsSize fs ≤ f) (rest : List Char) (hrest : ∃ (r : List Char), rest = ']' :: r) :

parseFields f ((Js.TyDesc.renderFields fs).toList ++ rest) = some (fs, rest)

Used by

Fold specs #

A spec carries the shape TyAlts does with a kind where a descriptor sits, so the reader is the descriptor's with the descent taken out: a kind is one of three words and nothing below it nests. The budget is still the spec's own size, because the recursion is on the text rather than on the tree.

The spec is printed as an object rather than as nested arrays, because __fold indexes it by the constructor's name, so the end of an empty one is told from the start of an entry the way parseObjFields tells them apart — by the space that opens }.

def

Lean2Js.Parse.foldFieldsSize

:

Js.FoldFields → Nat

Equations

Lean2Js.Parse.foldFieldsSize [] = 1
Lean2Js.Parse.foldFieldsSize (head :: rest) = Lean2Js.Parse.foldFieldsSize rest + 1

Instances For

Used by

def

Lean2Js.Parse.specSize

:

Js.FoldSpec → Nat

Equations

Lean2Js.Parse.specSize [] = 1
Lean2Js.Parse.specSize ((fst, fs) :: rest) = Lean2Js.Parse.foldFieldsSize fs + Lean2Js.Parse.specSize rest + 1

Instances For

Used by

theorem

Lean2Js.Parse.foldFieldsSize_pos

(fs : Js.FoldFields) :

0 < foldFieldsSize fs

Used by

theorem

Lean2Js.Parse.specSize_pos

(spec : Js.FoldSpec) :

0 < specSize spec

Used by

def

Lean2Js.Parse.parseFoldKind

:

List Char → Option (Js.FoldKind × List Char)

The three words FoldKind.render writes. A fourth is a text this printer does not write, so the reader has nothing to give back for it.

Equations

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

Instances For

Used by

theorem

Lean2Js.Parse.parseFoldKind_cons

(k : Js.FoldKind) (tail : List Char) :

parseFoldKind ('\"' :: (k.render.toList ++ '\"' :: tail)) = some (k, tail)

Used by

def

Lean2Js.Parse.parseFoldFields

:

Nat → List Char → Option (Js.FoldFields × List Char)

Equations

One or more equations did not get rendered due to their size.
Lean2Js.Parse.parseFoldFields 0 x✝ = none
Lean2Js.Parse.parseFoldFields f.succ (']' :: tail) = some ([], ']' :: tail)

Instances For

Used by

def

Lean2Js.Parse.parseFoldSpec

:

Nat → List Char → Option (Js.FoldSpec × List Char)

Equations

One or more equations did not get rendered due to their size.
Lean2Js.Parse.parseFoldSpec 0 x✝ = none
Lean2Js.Parse.parseFoldSpec f.succ (' ' :: tail) = some ([], ' ' :: tail)

Instances For

Used by

theorem

Lean2Js.Parse.parseFoldFields_append

(fs : Js.FoldFields) (f : Nat) (hf : foldFieldsSize fs ≤ f) (rest : List Char) (hrest : ∃ (r : List Char), rest = ']' :: r) :

parseFoldFields f ((Js.renderFoldFields fs).toList ++ rest) = some (fs, rest)

Used by

theorem

Lean2Js.Parse.parseFoldSpec_append

(spec : Js.FoldSpec) (f : Nat) (hf : specSize spec ≤ f) (rest : List Char) (hrest : ∃ (r : List Char), rest = ' ' :: r) :

parseFoldSpec f ((Js.renderFoldSpec spec).toList ++ rest) = some (spec, rest)

Used by

Expressions #

The grammar is fully parenthesised and has no optional whitespace, so one character of lookahead picks the form everywhere except after (, where arrowHead reads ahead for (names) => (. Nothing else the printer writes has that shape: member closes with )., and binary and cond put a space where the arrow wants ).

def

Lean2Js.Parse.isOpChar

(c : Char) :

Equations

Lean2Js.Parse.isOpChar c = (c == '+' || c == '-' || c == '*' || c == '/' || c == '%' || c == '<' || c == '>' || c == '=' || c == '!' || c == '&' || c == '|')

Instances For

Used by

def

Lean2Js.Parse.parseOpChars

:

List Char → List Char × List Char

Equations

Lean2Js.Parse.parseOpChars [] = ([], [])
Lean2Js.Parse.parseOpChars (c :: rest) = if Lean2Js.Parse.isOpChar c = true then match Lean2Js.Parse.parseOpChars rest with | (ds, r) => (c :: ds, r) else ([], c :: rest)

Instances For

Used by

def

Lean2Js.Parse.parseOp

(cs : List Char) :

Option (String × List Char)

Equations

Lean2Js.Parse.parseOp cs = match Lean2Js.Parse.parseOpChars cs with | (ds, r) => if ds.isEmpty = true then none else some (String.ofList ds, r)

Instances For

Used by

def

Lean2Js.Parse.parseNumeral

(cs : List Char) :

Option (Js.Expr × List Char)

Equations

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

Instances For

Used by

def

Lean2Js.Parse.negateNumeral

:

Js.Expr → Option Js.Expr

Undoes the sign a numeral reader takes with it, for the one place where (- opens a unary minus rather than a negative literal.

Equations

Lean2Js.Parse.negateNumeral (Lean2Js.Js.Expr.num i) = some (Lean2Js.Js.Expr.num (-i))
Lean2Js.Parse.negateNumeral (Lean2Js.Js.Expr.bigLit i) = some (Lean2Js.Js.Expr.bigLit (-i))
Lean2Js.Parse.negateNumeral x✝ = none

Instances For

Used by

def

Lean2Js.Parse.parseIdentList

:

Nat → List Char → Option (List String × List Char)

Equations

One or more equations did not get rendered due to their size.
Lean2Js.Parse.parseIdentList 0 x✝ = none

Instances For

Used by

def

Lean2Js.Parse.parseArrowHead

(f : Nat) (cs : List Char) :

Option (List String × List Char)

Equations

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

Instances For

Used by

def

Lean2Js.Parse.parseExpr

:

Nat → List Char → Option (Js.Expr × List Char)

Equations

One or more equations did not get rendered due to their size.
Lean2Js.Parse.parseExpr 0 x✝ = none
Lean2Js.Parse.parseExpr f.succ [] = none
Lean2Js.Parse.parseExpr f.succ ('\"' :: tail) = Option.map (fun (p : String × List Char) => (Lean2Js.Js.Expr.str p.fst, p.snd)) (Lean2Js.Parse.parseStr ('\"' :: tail))
Lean2Js.Parse.parseExpr f.succ ('(' :: r) = Lean2Js.Parse.parseParen f r

Instances For

Used by

def

Lean2Js.Parse.parseNamed

:

Nat → String → List Char → Option (Js.Expr × List Char)

What follows a name: a keyword, a helper the printer has a constructor for, a call, or the name itself.

Equations

One or more equations did not get rendered due to their size.
Lean2Js.Parse.parseNamed 0 x✝¹ x✝ = none

Instances For

Used by

def

Lean2Js.Parse.parseLambdaCall

:

Nat → List Char → Option (Js.Expr × String × Js.Expr × List Char)

Equations

One or more equations did not get rendered due to their size.
Lean2Js.Parse.parseLambdaCall 0 x✝ = none

Instances For

Used by

def

Lean2Js.Parse.parseParen

:

Nat → List Char → Option (Js.Expr × List Char)

Equations

One or more equations did not get rendered due to their size.
Lean2Js.Parse.parseParen 0 x✝ = none

Instances For

Used by

def

Lean2Js.Parse.parseAfterHead

:

Nat → Js.Expr → List Char → Option (Js.Expr × List Char)

The three forms that open with a subexpression: (e).f, (e op e) and (e ? e : e). A ) with no field behind it is the unary minus a numeral reader has already swallowed the sign of.

Equations

One or more equations did not get rendered due to their size.
Lean2Js.Parse.parseAfterHead 0 x✝¹ x✝ = none
Lean2Js.Parse.parseAfterHead f.succ x✝ (')' :: '.' :: r) = do let __x ← Lean2Js.Parse.parseIdent r match __x with | (field, r) => pure (x✝.member field, r)
Lean2Js.Parse.parseAfterHead f.succ x✝ (')' :: r) = Option.map (fun (e : Lean2Js.Js.Expr) => (Lean2Js.Js.Expr.unary "-" e, r)) (Lean2Js.Parse.negateNumeral x✝)
Lean2Js.Parse.parseAfterHead f.succ x✝¹ x✝ = none

Instances For

Used by

def

Lean2Js.Parse.parseExprList

:

Nat → Char → List Char → Option (List Js.Expr × List Char)

Equations

One or more equations did not get rendered due to their size.
Lean2Js.Parse.parseExprList 0 x✝¹ x✝ = none
Lean2Js.Parse.parseExprList f.succ x✝ [] = none

Instances For

Used by

def

Lean2Js.Parse.parseObjFields

:

Nat → List Char → Option (List (String × Js.Expr) × List Char)

Equations

One or more equations did not get rendered due to their size.
Lean2Js.Parse.parseObjFields 0 x✝ = none
Lean2Js.Parse.parseObjFields f.succ (' ' :: tail) = some ([], ' ' :: tail)

Instances For

Used by

def

Lean2Js.Parse.parseEntries

:

Nat → List Char → Option (List (String × Js.Expr) × List Char)

Equations

One or more equations did not get rendered due to their size.
Lean2Js.Parse.parseEntries 0 x✝ = none
Lean2Js.Parse.parseEntries f.succ (']' :: tail) = some ([], ']' :: tail)

Instances For

Used by

Statements, functions and the module #

The runtime helpers are matched as the one literal block the printer writes them as. The block is what Helper's own printer makes of the definitions the helper proofs are stated over, so it is an AST on the way out; the reader does not take it back apart, and accepting it verbatim is what "reads back exactly what this printer writes" means for that part.

def

Lean2Js.Parse.takeUntil

(lit : List Char) :

List Char → Option (List Char × List Char)

Equations

One or more equations did not get rendered due to their size.
Lean2Js.Parse.takeUntil lit [] = none

Instances For

Used by

def

Lean2Js.Parse.parseStmt

(f : Nat) (cs : List Char) :

Option (Js.Stmt × List Char)

Equations

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

Instances For

Used by

def

Lean2Js.Parse.parseStmts

:

Nat → List Char → Option (List Js.Stmt × List Char)

Equations

One or more equations did not get rendered due to their size.
Lean2Js.Parse.parseStmts 0 x✝ = none
Lean2Js.Parse.parseStmts f.succ ('\n' :: '}' :: tail) = some ([], '\n' :: '}' :: tail)

Instances For

Used by

def

Lean2Js.Parse.parseFunc

:

Nat → List Char → Option (Js.Func × List Char)

Equations

One or more equations did not get rendered due to their size.
Lean2Js.Parse.parseFunc 0 x✝ = none

Instances For

Used by

def

Lean2Js.Parse.parseFuncs

:

Nat → List Char → Option (List Js.Func × List Char)

Equations

One or more equations did not get rendered due to their size.
Lean2Js.Parse.parseFuncs 0 x✝ = none
Lean2Js.Parse.parseFuncs f.succ [] = some ([], [])

Instances For

Used by

def

Lean2Js.Parse.parseModule

(cs : List Char) :

Option Js.Module

Equations

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

Instances For

Used by

The grammar the reader accepts #

One case per printer branch, plus the places where two branches open with the same character. The theorem below covers these too; they are here because a reader that drifts from the printer stops building long before a proof about it does.