From e6ecef1fba79e99f93644a02723835cfec1c8a48 Mon Sep 17 00:00:00 2001
From: bringert <bringert@cs.chalmers.se>
Date: Mon, 13 Mar 2006 10:56:45 +0000
Subject: [PATCH] Transfer reflexive example: added ideal version.

---
 transfer/examples/reflexive/reflexive.tra | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/transfer/examples/reflexive/reflexive.tra b/transfer/examples/reflexive/reflexive.tra
index 9f8533f7a..8d28f0db0 100644
--- 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
+
+-}
\ No newline at end of file