Transfer reflexive example: added ideal version.

2006-03-13 10:56:45 +00:00
parent 941a9f35ba
commit eee0f20ea8
1 changed files with 9 additions and 0 deletions
--- a/transfer/examples/reflexive/reflexive.tra
+++ b/transfer/examples/reflexive/reflexive.tra
@@ -29,3 +29,12 @@ reflexivize _ t = composOp ? ? compos_Tree ? reflexivize t

 reflexivize_S : Tree S -> Tree S
 reflexivize_S = reflexivize S
+
+{-
+With a type checker and hidden arguments we could write:
+
+reflexivize : {C : Cat} -> Tree C -> Tree C
+reflexivize (PredV2 v s o) | s == o = ReflV2 v s
+reflexivize t = composOp reflexivize t
+
+-}