summaryrefslogtreecommitdiff
path: root/examples
diff options
context:
space:
mode:
Diffstat (limited to 'examples')
-rw-r--r--examples/test/typecheck/Check.gf14
1 files changed, 14 insertions, 0 deletions
diff --git a/examples/test/typecheck/Check.gf b/examples/test/typecheck/Check.gf
new file mode 100644
index 000000000..38d098209
--- /dev/null
+++ b/examples/test/typecheck/Check.gf
@@ -0,0 +1,14 @@
+abstract Check = {
+
+cat Typ ; Exp Typ ;
+
+fun plus : (t : Typ) -> (_,_ : Exp t) -> Exp t ;
+
+fun TInt, TFloat : Typ ;
+
+fun Zero : Exp TInt ;
+fun Pi : Exp TFloat ;
+
+fun sqrt : Exp TFloat -> Exp TFloat ;
+
+}