diff options
Diffstat (limited to 'src/Core')
| -rw-r--r-- | src/Core/Var.idr | 26 |
1 files changed, 26 insertions, 0 deletions
diff --git a/src/Core/Var.idr b/src/Core/Var.idr index 4e357aa..e1f45a0 100644 --- a/src/Core/Var.idr +++ b/src/Core/Var.idr @@ -45,6 +45,32 @@ view : (i : Var sx) -> View i view (MakeVar 0 Here) = Here view (MakeVar (S k) (There prf)) = There (MakeVar k prf) +-- Views are Unique + +viewInverse : {0 i : Var sx} -> View i -> Var sx +viewInverse Here = here +viewInverse (There i) = there i + +viewInversePrf1 : (view : View i) -> viewInverse view = i +viewInversePrf1 Here = Refl +viewInversePrf1 (There i) = Refl + +viewInversePrf2 : + {0 i : Var sx} -> + (v : View i) -> + view (viewInverse v) = (rewrite viewInversePrf1 v in v) +viewInversePrf2 Here = Refl +viewInversePrf2 (There (MakeVar index prf)) = Refl + +export +viewUnique : {0 i : Var sx} -> (view1, view2 : View i) -> view1 = view2 +viewUnique view1 view2 = + rewrite sym $ viewInversePrf2 view1 in + rewrite sym $ viewInversePrf2 view2 in + rewrite viewInversePrf1 view1 in + rewrite viewInversePrf1 view2 in + Refl + -- Operations ------------------------------------------------------------------ doWkn : Var sx -> {0 thin : sx `Thins` sy} -> View thin -> Var sy |