Idris2Doc : Pipeline.Equality

Pipeline.Equality

Equality pipelines hardcoded to avoid as much instance search as possible

Reexports

import public Data.Vect
import public Data.Vect.Quantifiers
import public Data.Vect.Utils

ProofSpec : Nat -> Type -> Type: Visibility: public export
ProofSteps : ProofSpec n a -> Type: Visibility: public export
Prove : (spec : ProofSpec n a) -> ProofSteps spec -> head spec = last spec: Visibility: public export