mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-14 22:02:07 +03:00
43 lines
893 B
Plaintext
43 lines
893 B
Plaintext
testlet : Integer -> Integer
|
|
testlet $x = let y = prim__add_Integer x x in
|
|
prim__add_Integer y y
|
|
|
|
data Nat : Type where
|
|
Z : Nat
|
|
S : Nat -> Nat
|
|
|
|
plus : Nat -> Nat -> Nat
|
|
plus Z $y = y
|
|
plus (S $k) $y = S (plus k y)
|
|
|
|
fn2 : Nat -> Nat -> Nat
|
|
fn2 $x $y
|
|
= let w : Nat
|
|
w = plus x x;
|
|
help : Nat -> Nat
|
|
help $z = plus z w in
|
|
plus (help y) w
|
|
|
|
fn : Nat -> Nat -> Nat
|
|
fn $x $y
|
|
= let w : ?; w = plus x x in
|
|
let foo = plus x x in
|
|
let help : Nat -> Nat;
|
|
help $z = plus z w in
|
|
plus (help y) foo
|
|
|
|
localdata : Nat -> Nat
|
|
localdata $var =
|
|
let data Bool : Type where
|
|
False : Bool
|
|
True : Bool
|
|
|
|
isS : Nat -> Bool
|
|
isS Z = False
|
|
isS (S $k) = True
|
|
|
|
boolToNat : Bool -> Nat
|
|
boolToNat False = Z
|
|
boolToNat True = S var in
|
|
boolToNat (isS var)
|