Skip to content

Instantly share code, notes, and snippets.

@bigs
Created August 16, 2020 16:56
Show Gist options
  • Save bigs/316bf0295514ef35e3237774e1546092 to your computer and use it in GitHub Desktop.
Save bigs/316bf0295514ef35e3237774e1546092 to your computer and use it in GitHub Desktop.
module Adder
AdderType : Nat -> Type
AdderType 0 = Int
AdderType (S k) = Int -> AdderType k
adder : {n : Nat} -> {default 0 acc : Int} -> AdderType n
adder {n=Z} {acc} = acc
adder {n=S k} {acc} = \x => adder {n=k} {acc=acc + x}
-- adder {n=3} 3 5 7
-- 15
@bigs
Copy link
Author

bigs commented Aug 16, 2020

Vect> adder {n=2} 3 4 8 
(interactive):1:1--1:18:When unifying Int and ?argTy -> ?retTy
Mismatch between:
        Int
and
        ?argTy -> ?retTy
at:
1       adder {n=2} 3 4 8
        ^^^^^^^^^^^^^^^^^

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment