SplitOnDotPattern.agda

-- When checking pattern coverage we might end up having to split
-- on a dot pattern (if the individual clauses split differently).
-- This is fine as long as the dot pattern is on constructor form.
module SplitOnDotPattern where

data Nat : Set where
  zero : Nat
  suc  : Nat -> Nat

data Vec (A : Set) : Nat -> Set where
  []   : Vec A zero
  _::_ : forall {n} -> A -> Vec A n -> Vec A (suc n)

rev : forall {A n m} -> Vec A n -> Vec A m -> Vec A m
rev             []        ys = ys
rev {n = suc n} (x :: xs) ys = ys