Version: dev

This is the documentation for the development version. For the latest release, see v0.12.1.

The token-level round trip

Lean module Esm.Document.Math.Main, formal/Esm/Document/Math/Main.lean at 184aa13d35e5
Imports Esm.Document.Math.Atoms

def addAcc source
def addAcc (e : Json) : List Json

The pending + operands a level-4 parse of e leaves in the loop.

def PA source
def PA (c : Ctx) (e : Json) : Prop

The level-4 parse of e stops in the + loop, with fuel to spare.

def PCr source
def PCr (c : Ctx) (e : Json) : Prop

e as the last rows of a cases block reads back.

def M source
def M (c : Ctx) (e : Json) : Prop

Everything the induction carries.

Generic steps

This module also proves 2 lemmas without doc comments; they are in the source.