Skip to content

Commit

Permalink
compile singe argument function - update Hello example
Browse files Browse the repository at this point in the history
  • Loading branch information
lemastero committed Dec 15, 2023
1 parent 61ee734 commit 0069f23
Show file tree
Hide file tree
Showing 2 changed files with 22 additions and 8 deletions.
14 changes: 9 additions & 5 deletions test/Hello.agda
Original file line number Diff line number Diff line change
@@ -1,11 +1,15 @@
module test.Hello where

-- simple record type
data Rgb : Set where
red green blue : Rgb
{-# COMPILE AGDA2RUST Rgb #-}
data TheRgb : Set where
red green blue : TheRgb
{-# COMPILE AGDA2RUST TheRgb #-}

data TheWeekDay : Set where
Monday Tuesday Wednesday Thursday Friday Saturday Sunday : TheWeekDay
{-# COMPILE AGDA2RUST TheWeekDay #-}

-- simple function
idRgb : Rgb Rgb
idRgb x = x
idRgb : TheRgb TheRgb
idRgb rgbArg = rgbArg
{-# COMPILE AGDA2RUST idRgb #-}
16 changes: 13 additions & 3 deletions test/Hello.rs
Original file line number Diff line number Diff line change
@@ -1,12 +1,22 @@
mod test.Hello {
enum Rgb {
enum TheRgb {
red, green, blue
}



pub fn idRgb((x : test.Hello.Rgb) |- x@0 = @0 : test.Hello.Rgb) {
done[x] @0
enum TheWeekDay {
Monday, Tuesday, Wednesday, Thursday, Friday, Saturday, Sunday
}







pub fn idRgb(rgbArg: TheRgb): TheRgb {
return rgbArg
}


Expand Down

0 comments on commit 0069f23

Please sign in to comment.