From 0419860b4e1463ef5c9f32e0697f917806b78752 Mon Sep 17 00:00:00 2001 From: bringert Date: Mon, 20 Mar 2006 18:23:55 +0000 Subject: Transfer: some TODOs. Lots of minor fixes in type checking algorithm. --- transfer/examples/tricky-type-checking.tra | 6 ++++++ 1 file changed, 6 insertions(+) (limited to 'transfer/examples') diff --git a/transfer/examples/tricky-type-checking.tra b/transfer/examples/tricky-type-checking.tra index 4cc8037ba..ad69c33db 100644 --- a/transfer/examples/tricky-type-checking.tra +++ b/transfer/examples/tricky-type-checking.tra @@ -8,6 +8,12 @@ data Tree : Type -> Type where EInt : Integer -> Tree Integer EFoo : (A:Type) -> A -> Tree A +eval : (B : Type) -> Tree B -> Tree B +eval _ t = case t of + EAdd x y -> EInt (x+y) + EInt i -> EInt i + EFoo T x -> EFoo T x + strip : (B : Type) -> Tree B -> B strip _ t = case t of EAdd x y -> x+y -- cgit v1.2.3