diff options
Diffstat (limited to 'src/Core/LogRel/View.idr')
| -rw-r--r-- | src/Core/LogRel/View.idr | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/src/Core/LogRel/View.idr b/src/Core/LogRel/View.idr index 1790c9f..64e6c97 100644 --- a/src/Core/LogRel/View.idr +++ b/src/Core/LogRel/View.idr @@ -36,7 +36,7 @@ view (RedNtrlTy red1) (RedNtrlTy red2) (EqNtrlTy tyEq) = Ntrl red1 red2 view (RedNtrlTy red1) (RedSetTy red2) (EqNtrlTy tyEq) = let det : (Set = tyEq.b') - det = typeRedDeterministic red2.steps tyEq.steps Set (Ntrl tyEq.ntrl) + det = typeRedDeterministic red2.stepsWf.steps tyEq.stepsWf.steps Set (Ntrl tyEq.ntrl) ntrl : Neutral (Set {n}) ntrl = rewrite det in tyEq.ntrl @@ -45,7 +45,7 @@ view (RedNtrlTy red1) (RedSetTy red2) (EqNtrlTy tyEq) = view (RedNtrlTy red1) (RedPiTy red2) (EqNtrlTy tyEq) = let det : (Pi red2.f red2.g = tyEq.b') - det = typeRedDeterministic red2.steps tyEq.steps Pi (Ntrl tyEq.ntrl) + det = typeRedDeterministic red2.stepsWf.steps tyEq.stepsWf.steps Pi (Ntrl tyEq.ntrl) ntrl : Neutral (Pi red2.f red2.g) ntrl = rewrite det in tyEq.ntrl @@ -54,7 +54,7 @@ view (RedNtrlTy red1) (RedPiTy red2) (EqNtrlTy tyEq) = view (RedSetTy red1) (RedNtrlTy red2) (EqSetTy tyEq) = let det : (red2.a' = Set) - det = typeRedDeterministic red2.steps tyEq.steps (Ntrl red2.ntrl) Set + det = typeRedDeterministic red2.stepsWf.steps tyEq.stepsWf.steps (Ntrl red2.ntrl) Set ntrl : Neutral (Set {n}) ntrl = rewrite sym det in red2.ntrl @@ -64,13 +64,13 @@ view (RedSetTy red1) (RedSetTy red2) (EqSetTy tyEq) = Set red1 red2 view (RedSetTy red1) (RedPiTy red2) (EqSetTy tyEq) = let det : (Pi red2.f red2.g = Set) - det = typeRedDeterministic red2.steps tyEq.steps Pi Set + det = typeRedDeterministic red2.stepsWf.steps tyEq.stepsWf.steps Pi Set in absurd det view (RedPiTy red1) (RedNtrlTy red2) (EqPiTy tyEq) = let det : (red2.a' = Pi tyEq.f tyEq.g) - det = typeRedDeterministic red2.steps tyEq.steps (Ntrl red2.ntrl) Pi + det = typeRedDeterministic red2.stepsWf.steps tyEq.stepsWf.steps (Ntrl red2.ntrl) Pi ntrl : Neutral (Pi tyEq.f tyEq.g) ntrl = rewrite sym det in red2.ntrl @@ -79,7 +79,7 @@ view (RedPiTy red1) (RedNtrlTy red2) (EqPiTy tyEq) = view (RedPiTy red1) (RedSetTy red2) (EqPiTy tyEq) = let det : (Set = Pi tyEq.f tyEq.g) - det = typeRedDeterministic red2.steps tyEq.steps Set Pi + det = typeRedDeterministic red2.stepsWf.steps tyEq.stepsWf.steps Set Pi in absurd det view (RedPiTy red1) (RedPiTy red2) (EqPiTy tyEq) = Pi red1 red2 |