
  0 | ||| Equality pipelines hardcoded to avoid as much instance search as possible
  1 | 
  2 | module Pipeline.Equality
  3 | 
  4 | import public Data.Vect
  5 | import Control.Category
  6 | import public Data.Vect.Quantifiers
  7 | import public Data.Vect.Utils
  8 | 
  9 | public export
 10 | ProofSpec : Nat -> Type -> Type
 11 | ProofSpec n = Vect (2 + n)
 12 | 
 13 | public export
 14 | ProofSteps : ProofSpec n a -> Type
 15 | ProofSteps = All (uncurry (Equal {a, b = a})) . pairUp
 16 | 
 17 | public export
 18 | Prove : (spec : ProofSpec n a) -> ProofSteps spec -> Vect.head spec === Vect.last spec
 19 | Prove [x, y] [p] = p
 20 | Prove (y :: (z :: (v :: xs))) (x :: (w :: s)) =
 21 |   trans x (Prove (z :: v :: xs) (w :: s))
 22 | 
 23 | -- In case you want to use the generic version we provide a category instance
 24 | public export
 25 | Category Equal where
 26 |   id = Refl
 27 |   (.) Refl Refl = Refl
 28 |