diff options
| author | bringert <bringert@cs.chalmers.se> | 2006-03-13 10:56:45 +0000 |
|---|---|---|
| committer | bringert <bringert@cs.chalmers.se> | 2006-03-13 10:56:45 +0000 |
| commit | eee0f20ea84b2540acf5fb6b969755adeebb2e5b (patch) | |
| tree | 2fb52730f631cbc35dc92a01bddc642d03df6368 | |
| parent | 941a9f35baa4a67c1ee5df89f1ae0f40677a214d (diff) | |
Transfer reflexive example: added ideal version.
| -rw-r--r-- | transfer/examples/reflexive/reflexive.tra | 9 |
1 files changed, 9 insertions, 0 deletions
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 |