[Agda] [agda2] how to programming the basic

[Sergei Meshveliani]

On Wed, 2016-01-27 at 12:50 +0000, Mandy Martino wrote:
> Hi Sergei,
> 
> 1.
> i defined  mutual  block  but  can not parse.
> 
> Could not parse the application m +2 n *2 m
> when scope checking m +2 n *2 m
> 
> 2. when comment above error code , and continue to run, it has  error at  if2_then2_else2_ Bool2 true (putStrLn "it is true") (putStrLn "it is else case")
> Type mismatch
> when checking that the pattern true has type Set
> 
> open import Prelude
> 
> data Bool2 : Set where
>  true : Bool2
>  false : Bool2
> 
> not2 : Bool2 -> Bool2
> not2 true = false
> not2 false = true
> 
> identity2 : (A : Set) -> A -> A
> identity2 A x = x
> 
> data Nat2 : Set where
>  zero2 : Nat2
>  suc : Nat2 -> Nat2
> 
> mutual
>  _+2_ : Nat2 -> Nat2 -> Nat2
>  zero2 +2 m = zero2
>  suc n +2 m = suc (n +2 m)
> 
>  _*2_ : Nat2 -> Nat2 -> Nat2
>  zero2 *2 m = zero2
>  suc n *2 m = m +2 n *2 m
> 

1) Set this last line as

   suc n *2 m = m +2 (n *2 m)

2) For this example, `mutual' is not necessary.


> [..]
>
> if2_then2_else2_ : (A : Set) -> Bool2 -> A -> A -> A
> if2 true then2 x else2 y = x
> if2 false then2 x else2 y = y
> 
> main = 
>  if2_then2_else2_ Bool2 true (putStrLn "it is true") (putStrLn "it is else case")
>  putStrLn "Hello World"

if2_then2_else2_  is declared with 4 arguments and is called with 3
arguments. See my previous letter(s).

Regards,

------
Sergei