rename and0 to constRgbPair

lemastero · May 6, 2024 · 2b7e44c · 2b7e44c
1 parent fb8d09e
commit 2b7e44c
Showing 1 changed file with 4 additions and 3 deletions.
diff --git a/examples/adts.agda b/examples/adts.agda
@@ -42,6 +42,7 @@ rgbConstTrue1 rgb = True -- TODO produce function body
 
 -- function with multiple named arguments
 
-and0 : (rgbPairArg : RgbPair) -> (rgbArg : Rgb) -> RgbPair
-and0 rgbPairArg rgbArg = rgbPairArg
-{-# COMPILE AGDA2SCALA and0 #-}
+constRgbPair : (rgbPairArg : RgbPair) -> (rgbArg : Rgb) -> RgbPair
+constRgbPair rgbPairArg rgbArg = rgbPairArg
+{-# COMPILE AGDA2SCALA constRgbPair #-}
+ľ