PrimParser Lawfulness Proofs

Lawful instances for Success, Outcome, and Parser: LawfulFunctor, LawfulGradedFunctor, LawfulGradedApplicative, LawfulGradedMonad.

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

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

instance Parser.instLawfulGradedFunctorNecessitySuccess {n : ℕ} : LawfulGradedFunctor (Success n)

instance Parser.instLawfulGradedFunctorGrade {ε : Type} : LawfulGradedFunctor (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.instLawfulGradedApplicativeGrade {ε : Type} : LawfulGradedApplicative (Parser ε)

instance Parser.instLawfulGradedMonadGrade {ε : Type} : LawfulGradedMonad (Parser ε)