PrimParser Lawfulness Proofs

Lawful instances for Success, Outcome, and Parser: LawfulFunctor, LawfulGFunctor, LawfulGApplicative, LawfulGMonad.

instance Parser.instLawfulFunctorSuccess {n : ℕ} {gc : Necessity} : LawfulFunctor (Success n gc)

instance Parser.instLawfulFunctorOutcome {ε : Type} {n : ℕ} {g : Grade} : LawfulFunctor (Outcome ε n g)

instance Parser.instLawfulGFunctorNecessitySuccess {n : ℕ} : LawfulGFunctor (Success n)

instance Parser.instLawfulGFunctorGrade {ε : Type} : LawfulGFunctor (Parser ε)

theorem Parser.gbind_assoc {α β γ ε : Type} {ge1 gc1 ge2 gc2 ge3 gc3 : Necessity} (p1 : Parser ε { errors := ge1, consumes := gc1 } α) (p2 : α → Parser ε { errors := ge2, consumes := gc2 } β) (p3 : β → Parser ε { errors := ge3, consumes := gc3 } γ) : p1 >>=ᵍ p2 >>=ᵍ p3 ≍ p1 >>=ᵍ fun (a : α) => p2 a >>=ᵍ p3

instance Parser.instLawfulGApplicativeGrade {ε : Type} : LawfulGApplicative (Parser ε)

instance Parser.instLawfulGMonadGrade {ε : Type} : LawfulGMonad (Parser ε)