diff options
Diffstat (limited to 'transfer')
| -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 |