diff options
| author | Chloe Brown <chloe.brown.00@outlook.com> | 2023-04-23 15:23:57 +0100 |
|---|---|---|
| committer | Chloe Brown <chloe.brown.00@outlook.com> | 2023-04-23 15:23:57 +0100 |
| commit | 6868d98d83ca64af4becf1b112f02b495e812f11 (patch) | |
| tree | 394fc8ffdd8b016f0227fe00eafca5c104a200f4 /src/Core/LogRel | |
| parent | dddc8083b56f265e1e53cd3e6d2e374b25f42cb3 (diff) | |
Bundle well-formed reductions.nameless
Diffstat (limited to 'src/Core/LogRel')
| -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 |