From 2b7e44c5c30c65888d67b5e1b6398836b9ccdbd5 Mon Sep 17 00:00:00 2001 From: lemastero Date: Mon, 6 May 2024 03:12:33 +0200 Subject: [PATCH] rename and0 to constRgbPair --- examples/adts.agda | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/examples/adts.agda b/examples/adts.agda index 754c4f5..3e8b3c5 100644 --- 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 #-} +ΔΎ \ No newline at end of file