From 6868d98d83ca64af4becf1b112f02b495e812f11 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Sun, 23 Apr 2023 15:23:57 +0100
Subject: Bundle well-formed reductions.

---
 src/Core/LogRel/View.idr | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

(limited to 'src/Core/LogRel/View.idr')

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
-- 
cgit v1.2.3