Parsing at a level, what may follow, and moving between levels
pLvl L parses at precedence level L (1 = an or chain … 9 = postfix, 10 =
a primary). Fol sf L rest says rest does not continue an expression parsed at
level L. lift
moves a parse at a tighter level to a looser one: the loops of the
levels in between stop at once.
def conts (sf : Sf) (L : Nat) : Tok → Bool
t continues an expression parsed at level L.
def Fol (sf : Sf) (L : Nat) (rest : List Tok) : Prop
rest does not continue an expression parsed at level L.
No level starts with a binary - or a not it does not own
Lifting a parse to a looser level
theorem negTail_fol {sf : Sf} {L : Nat} {r : List Tok} (hr : Fol sf L r) (hL : L ≤ 5) :
negTail r = none
Nothing that does not continue a level-5 parse starts with a number.