caledon-3.1.0.0: prelude/concatable.ncc

#include <naturals.ncc>
#include <list.ncc>

--------------
--- concat ---
--------------

defn concatable : [M : prop] (M -> M -> M -> prop) -> prop
  >| concatableNat = concatable natural add
  >| concatableList = concatable (list A) concatList

-- it correctly infers 169, and M (but it eta expands Foo when it infers it) !!
fixity right 3 ++
defn ++ : {M}{Foo}{cm : concatable M Foo} M -> M -> M -> prop
   | ppimp = [M][Foo : M -> M -> M -> prop][M1 M2 M3 : M] 
               (++) {Foo = Foo} M1 M2 M3 
            <- concatable M Foo 
            <- Foo M1 M2 M3