rudimentary abstract syntax type checker and solver in PGF

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 ;
+
+}