[Agda] [agda2] how to programming the basic

[Mandy Martino]

Hi Sergei,

i avoid multiple definition, i append 2 to all names, but do not know how to correct this ,
already defined zero2, still have error

Skipping Prelude (/home/martin/hilbertreborn/agda-prelude/src/Prelude.agdai).
/home/martin/hilbertreborn/bb.agda:19,1-19
Missing type signature for left hand side zero2 *2 m
when scope checking the declaration
  zero2 *2 m = zero2

real	0m0.738s
user	0m0.192s
sys	0m0.212s


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

_+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

_or2_ : Bool2 -> Bool2 -> Bool2
false or2 x = x
true or2 _ = true

if_then_else_ : (A : Set) -> Bool2 -> A -> A -> A
if true then x else y = x
if false then x else y = y

main = 
 if_then_else_ Bool2 true (putStrLn "it is true") (putStrLn "it is else case")
 putStrLn "Hello World"

Regards,

Martin 

________________________________________
寄件者: mechvel at scico.botik.ru <mechvel at scico.botik.ru>
寄件日期: 2016年1月23日 1:03
收件者: Mandy Martino
副本: agda at lists.chalmers.se
主旨: Re: [Agda] [agda2] how to programming the basic

Mandy Martino писал 22.01.2016 12:48:
> Hi ,
>
> when i am thinking new axiom to replace trans in Equality.agda
> ((a→b) ≡ b)→((a ≡ a) ≡ c)
> do not understand how can this replace equal, feel difficult to read
> standard library
>
> then i start
> http://www.cse.chalmers.se/~ulfn/papers/afp08/tutorial.pdf [1]
>
> do not know why it do not print "it is true"
>
> open import Prelude
>
> data Bool : Set where
>  true : Bool
>  false : Bool
>
> [..]
>
> if_then_else_ : (A : Set) -> Bool -> A -> A -> A
> if true then x else y = x
> if false then x else y = y
>
> main =
>  if true then putStrLn "it is true" else putStrLn "it is else case"
>  putStrLn "Hello World"
>


1) if_then_else_  declares 4 arguments, and you call it giving it 3
arguments.

2) For this `main' call, one must find and set the type of the data
    (putStrLn "it is true").

To avoid these complication, one can program, for example, this:

   if_then_else_ : {A : Set} → Bool → A → A → A
   if true  then x else y = x
   if false then x else y = y

Here the first argument is declared as implicit, with using `{}'.

   str : String
   str = if true then "it is true" else "it is else case"

   main = putStrLn (toCostring str)

Regards,

------
Sergei