[Agda] [agda2] how to programming the basic

[mechvel at scico.botik.ru]

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