1 files changed, 45 insertions, 45 deletions
diff --git a/src/Obs/Abstract.idr b/src/Obs/Abstract.idr
index a9ef411..f91be66 100644
--- a/src/Obs/Abstract.idr
+++ b/src/Obs/Abstract.idr
@@ -21,73 +21,73 @@ bind ctx str = (str, 0) :: map (mapSnd FS) ctx
 abstractSyntax : Context n -> Syntax -> Logging ann (Term n)
 abstractSyntaxBounds : Context n -> WithBounds Syntax -> Logging ann (WithBounds (Term n))
 
-abstractSyntax ctx (Var var) = do
+abstractSyntax ctx (Var {var}) = do
   let Just i = lookup var ctx
     | Nothing => inScope "unbound variable" $ fatal var
   pure (Var var i)
-abstractSyntax ctx (Universe s) = pure (Universe s)
-abstractSyntax ctx (Pi var a b) = do
-  a <- abstractSyntaxBounds ctx a
-  b <- abstractSyntaxBounds (bind ctx var.val) b
+abstractSyntax ctx (Universe {s}) = pure (Universe s)
+abstractSyntax ctx (Pi {var, domain, codomain}) = do
+  a <- abstractSyntaxBounds ctx domain
+  b <- abstractSyntaxBounds (bind ctx var.val) codomain
   pure (Pi var a b)
-abstractSyntax ctx (Lambda var t) = do
-  t <- abstractSyntaxBounds (bind ctx var.val) t
+abstractSyntax ctx (Lambda {var, body}) = do
+  t <- abstractSyntaxBounds (bind ctx var.val) body
   pure (Lambda var t)
-abstractSyntax ctx (App t u) = do
-  t <- abstractSyntaxBounds ctx t
-  u <- abstractSyntaxBounds ctx u
+abstractSyntax ctx (App {fun, arg}) = do
+  t <- abstractSyntaxBounds ctx fun
+  u <- abstractSyntaxBounds ctx arg
   pure (App t u)
-abstractSyntax ctx (Sigma var a b) = do
-  a <- abstractSyntaxBounds ctx a
-  b <- abstractSyntaxBounds (bind ctx var.val) b
+abstractSyntax ctx (Sigma {var, index, element}) = do
+  a <- abstractSyntaxBounds ctx index
+  b <- abstractSyntaxBounds (bind ctx var.val) element
   pure (Sigma var a b)
-abstractSyntax ctx (Pair t u) = do
-  t <- abstractSyntaxBounds ctx t
-  u <- abstractSyntaxBounds ctx u
+abstractSyntax ctx (Pair {first, second}) = do
+  t <- abstractSyntaxBounds ctx first
+  u <- abstractSyntaxBounds ctx second
   pure (Pair t u)
-abstractSyntax ctx (Fst t) = do
-  t <- abstractSyntaxBounds ctx t
+abstractSyntax ctx (First {arg}) = do
+  t <- abstractSyntaxBounds ctx arg
   pure (Fst t)
-abstractSyntax ctx (Snd t) = do
-  t <- abstractSyntaxBounds ctx t
+abstractSyntax ctx (Second {arg}) = do
+  t <- abstractSyntaxBounds ctx arg
   pure (Snd t)
 abstractSyntax ctx Bool = pure Bool
 abstractSyntax ctx True = pure True
 abstractSyntax ctx False = pure False
-abstractSyntax ctx (If var a t f g) = do
-  a <- abstractSyntaxBounds (bind ctx var.val) a
-  t <- abstractSyntaxBounds ctx t
-  f <- abstractSyntaxBounds ctx f
-  g <- abstractSyntaxBounds ctx g
+abstractSyntax ctx (If {var, returnType, discriminant, true, false}) = do
+  a <- abstractSyntaxBounds (bind ctx var.val) returnType
+  t <- abstractSyntaxBounds ctx discriminant
+  f <- abstractSyntaxBounds ctx true
+  g <- abstractSyntaxBounds ctx false
   pure (If var a t f g)
 abstractSyntax ctx Top = pure Top
 abstractSyntax ctx Point = pure Point
 abstractSyntax ctx Bottom = pure Bottom
-abstractSyntax ctx (Absurd t) = do
-  t <- abstractSyntaxBounds ctx t
+abstractSyntax ctx (Absurd {contradiction}) = do
+  t <- abstractSyntaxBounds ctx contradiction
   pure (Absurd t)
-abstractSyntax ctx (Equal t u) = do
-  t <- abstractSyntaxBounds ctx t
-  u <- abstractSyntaxBounds ctx u
+abstractSyntax ctx (Equal {left, right}) = do
+  t <- abstractSyntaxBounds ctx left
+  u <- abstractSyntaxBounds ctx right
   pure (Equal t u)
-abstractSyntax ctx (Refl t) = do
-  t <- abstractSyntaxBounds ctx t
+abstractSyntax ctx (Refl {value}) = do
+  t <- abstractSyntaxBounds ctx value
   pure (Refl t)
-abstractSyntax ctx (Transp a t u t' e) = do
-  a <- abstractSyntaxBounds ctx a
-  t <- abstractSyntaxBounds ctx t
-  u <- abstractSyntaxBounds ctx u
-  t' <- abstractSyntaxBounds ctx t'
-  e <- abstractSyntaxBounds ctx e
+abstractSyntax ctx (Transp {indexedType, oldIndex, value, newIndex, equality}) = do
+  a <- abstractSyntaxBounds ctx indexedType
+  t <- abstractSyntaxBounds ctx oldIndex
+  u <- abstractSyntaxBounds ctx value
+  t' <- abstractSyntaxBounds ctx newIndex
+  e <- abstractSyntaxBounds ctx equality
   pure (Transp a t u t' e)
-abstractSyntax ctx (Cast a b e t) = do
-  a <- abstractSyntaxBounds ctx a
-  b <- abstractSyntaxBounds ctx b
-  e <- abstractSyntaxBounds ctx e
-  t <- abstractSyntaxBounds ctx t
+abstractSyntax ctx (Cast {oldType, newType, equality, value}) = do
+  a <- abstractSyntaxBounds ctx oldType
+  b <- abstractSyntaxBounds ctx newType
+  e <- abstractSyntaxBounds ctx equality
+  t <- abstractSyntaxBounds ctx value
   pure (Cast a b e t)
-abstractSyntax ctx (CastId t) = do
-  t <- abstractSyntaxBounds ctx t
+abstractSyntax ctx (CastId {value}) = do
+  t <- abstractSyntaxBounds ctx value
   pure (CastId t)
 
 abstractSyntaxBounds ctx (MkBounded v irrel bnds) =