gistfile1.txt

- + Errors (1)
 `-- tutorial.idr line 24 col 20:
     When elaborating right hand side of vectormanip.reverse, reverseAcc:
     Can't unify
             Vect (m + S n) a
     with
             Vect (S (plus m n)) a
     
     Specifically:
             Can't unify
                     plus m (S n)
             with
                     S (plus m n)

reverse.idr

sPlusAssoc : (m, n: Nat) -> plus m (S n) = S (plus m n) 
sPlusAssoc Z n = refl
sPlusAssoc (S m) n = rewrite sPlusAssoc m n in refl

total reverse : Vect n a -> Vect n a
reverse xs = reverseAcc Nil xs where
        reverseAcc : Vect n a -> Vect m a -> Vect (m + n) a
        reverseAcc {n=n} {m=S m} acc (x :: xs) = reverseAcc (x :: acc) xs
        reverseAcc acc Nil       = acc

variations-that-dont-compile.idr

total reverse : Vect n a -> Vect n a
reverse xs = reverseAcc Nil xs where
        reverseAcc : Vect n a -> Vect m a -> Vect (m + n) a
        reverseAcc {n=n} {m=S m} acc (x :: xs) = 
                   rewrite sPlusAssoc m n in reverseAcc (x :: acc) xs
        reverseAcc acc Nil       = acc
        
-- - + Errors (1)
--  `-- tutorial.idr line 24 col 20:
--      When elaborating right hand side of vectormanip.reverse, reverseAcc:
--      rewrite did not change type Vect (S (plus m n)) a
        

total reverse : Vect n a -> Vect n a
reverse xs = reverseAcc Nil xs where
        reverseAcc : Vect n a -> Vect m a -> Vect (m + n) a
        reverseAcc {n=n} {m=S m} acc (x :: xs) = 
                   rewrite (sym sPlusAssoc m n) in reverseAcc (x :: acc) xs
        reverseAcc acc Nil       = acc
        
-- - + Errors (1)
--  `-- tutorial.idr line 25 col 28:
--      When elaborating right hand side of vectormanip.reverse, reverseAcc:
--      When elaborating an application of function sym:
--              Can't unify
--                      r = l
--              with
--                      argTy -> retTy
--              
--              Specifically:
--              Can't unify
--                              (=) r
--                      with
--                              \{uv0} => argTy -> uv


total reverse : Vect n a -> Vect n a
reverse xs = reverseAcc Nil xs where
        reverseAcc : Vect n a -> Vect m a -> Vect (m + n) a
        reverseAcc {n=(S n)} {m=m} acc (x :: xs) = 
                   rewrite (sym sPlusAssoc m n) in reverseAcc (x :: acc) xs
        reverseAcc acc Nil       = acc
        
-- - + Errors (1)
--  `-- tutorial.idr line 24 col 20:
--      When elaborating left hand side of vectormanip.reverse, reverseAcc:
--      When elaborating an application of vectormanip.reverse, reverseAcc:
--              Can't unify
--                      Vect (S n) a
--              with
--                      Vect m a
             
--              Specifically:
--                      Can't unify
--                              S n
--                      with
--                              m

total reverse : Vect n a -> Vect n a
reverse xs = reverseAcc Nil xs where
        reverseAcc : Vect n a -> Vect m a -> Vect (m + n) a
        reverseAcc {n=(S n)} {m=m} acc (x :: xs) = 
                   rewrite sPlusAssoc m n in reverseAcc (x :: acc) xs
        reverseAcc acc Nil       = acc

-- - + Errors (1)
--  `-- tutorial.idr line 24 col 20:
--      When elaborating left hand side of vectormanip.reverse, reverseAcc:
--      When elaborating an application of vectormanip.reverse, reverseAcc:
--              Can't unify
--                      Vect (S n) a
--              with
--                      Vect m a
             
--              Specifically:
--                      Can't unify
--                              S n
--                      with
--                              m