namespace http://cds.omdoc.org/examples❚

theory Equality : ur:?PLF =
  eq : {a: type} a ⟶ a ⟶ type ❘# 2 = 3 prec 0❘ role Eq❙
  reflexive : {a,x:a} x = x ❘# refl %I1 %I2❙
❚

theory List : ur:?PLF =
  include ?Equality❙
  list : type ⟶ type❙
  nil  : {a} list a❘# nil 1❙
  cons : {a} a ⟶ list a ⟶ list a❘# 2 %R, 3 prec 10❙

  embed : {a} a ⟶ list a ❘= [a,x] x , (nil a)❘# 2 | prec 20❙

  // the simplification rule generator does not allow fold to have implicit arguments yet❙
  fold : {a,b:type} list a ⟶ b ⟶ (a ⟶ b ⟶ b) ⟶ b❙
  fold_nil : {a:type,b,n:b,c: a ⟶ b ⟶ b} (fold a b (nil a) n c) = n❘ role Simplify❙
  fold_cons : {a,b,x,l,n,c:a ⟶ b ⟶ b} (fold a b (x,l) n c) = (c x (fold a b l n c))❘role Simplify❙
  
  concat : {a} list a ⟶ list a ⟶ list a❘= [a,l,m] fold a (list a) l m [x,xs] x,xs ❘# 2 + 3 prec 5❙

❚

theory Test : ur:?PLF =
  include ?List❙
  a : type❙
  c : a❙
  f : a ⟶ a❙

  test : (c,c|)+(c,c|) = c,c,c,c|❘= refl❙  
❚