diff options
| -rw-r--r-- | transfer/examples/tricky-type-checking.tra | 31 |
1 files changed, 31 insertions, 0 deletions
diff --git a/transfer/examples/tricky-type-checking.tra b/transfer/examples/tricky-type-checking.tra new file mode 100644 index 000000000..4cc8037ba --- /dev/null +++ b/transfer/examples/tricky-type-checking.tra @@ -0,0 +1,31 @@ + +-- +-- Pattern matching and inductive families. +-- + +data Tree : Type -> Type where + EAdd : Tree Integer -> Tree Integer -> Tree Integer + EInt : Integer -> Tree Integer + EFoo : (A:Type) -> A -> Tree A + +strip : (B : Type) -> Tree B -> B +strip _ t = case t of + EAdd x y -> x+y + EInt i -> i + EFoo _ x -> x + +-- +-- Subtyping +-- + +getX : { x : Integer } -> Integer +getX r = r.x + +getY : { y : Integer } -> Integer +getY r = r.y + +proj2 : (A:Type) -> (B:Type) -> (C:Type) -> (A -> B) -> (A -> C) -> A -> (B,C) +proj2 _ _ _ f g x = (f x, g x) + +getXY : { x : Integer, y : Integer } -> (Integer,Integer) +getXY r = proj2 ? ? ? getX getY r |