Lean module Esm.Document.Math.Cases2, formal/Esm/Document/Math/Cases2.lean at 184aa13d35e5
Imports Esm.Document.Math.Cases1
def kwStart (t : Tok) : Prop
A token that starts a keyword form.
This module also proves 13 lemmas without doc comments; they are in the source.