rename val to value

andrevidela · Nov 24, 2024 · a49d771 · a49d771
1 parent 471e473
commit a49d771
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 7 deletions.
diff --git a/libs/base/Language/Reflection/TT.idr b/libs/base/Language/Reflection/TT.idr
@@ -74,7 +74,7 @@ public export
 record WithFC (ty : Type) where
   constructor MkFCVal
   fc : FC
-  val : ty
+  value : ty
 
 ||| Smart constructor for WithFC that uses EmptyFC as location
 %inline export
@@ -83,11 +83,11 @@ NoFC = MkFCVal EmptyFC
 
 export
 Functor WithFC where
-  map f = { val $= f}
+  map f = { value $= f}
 
 export
 Foldable WithFC where
-  foldr f i v = f v.val i
+  foldr f i v = f v.value i
 
 export
 Traversable WithFC where

diff --git a/libs/base/Language/Reflection/TTImp.idr b/libs/base/Language/Reflection/TTImp.idr
@@ -415,7 +415,7 @@ parameters {auto eqTTImp : Eq TTImp}
 
   public export
   Eq ITy where
-    MkTy _ n ty == MkTy _ n' ty' = n.val == n'.val && ty == ty'
+    MkTy _ n ty == MkTy _ n' ty' = n.value == n'.value && ty == ty'
 
   public export
   Eq Data where
@@ -442,7 +442,7 @@ parameters {auto eqTTImp : Eq TTImp}
 
   public export
   Eq Decl where
-    IClaim c == IClaim c' = c.val == c'.val
+    IClaim c == IClaim c' = c.value == c'.value
     IData _ v t d == IData _ v' t' d' =
       v == v' && t == t' && d == d'
     IDef _ n cs == IDef _ n' cs' =
@@ -552,7 +552,7 @@ mutual
 
   public export
   Show ITy where
-    show (MkTy fc n ty) = "\{show n.val} : \{show ty}"
+    show (MkTy fc n ty) = "\{show n.value} : \{show ty}"
 
   Show IClaimData where
     show (MkIClaimData rig vis xs sig)
@@ -561,7 +561,7 @@ mutual
 
   public export
   Show Decl where
-    show (IClaim claim) = show claim.val
+    show (IClaim claim) = show claim.value
     show (IData fc vis treq dt)
       = unwords [ show vis
                 , showTotalReq treq (show dt)