[Agda] how to run this rewrite example

[Mandy Martino]

Hi ,


when run the code directly, it return missing definition,

how to write this definition?


bb.agda:26,1-13

Missing definition for plus-commute


Following

http://agda.readthedocs.org/en/latest/language/with-abstraction.html#rewrite

With-Abstraction - Agda 2.5 documentation<http://agda.readthedocs.org/en/latest/language/with-abstraction.html#rewrite>
agda.readthedocs.org
The clause containing the with-abstraction has no right-hand side. Instead it is followed by a number of clauses with an extra argument on the left, separated from ...


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

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

if2_then2_else2_ : (A : Set) -> Bool2 -> A -> A -> A
if2 true then2 x else2 y = x
if2 false then2 x else2 y = y

plus-commute : (a b : Nat) ? a + b ? b + a

thm : (a b : Nat) ? P (a + b) ? P (b + a)
thm a b t with   a + b  | plus-commute a b
thm a b t    | .(b + a) | refl = t

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



Regards,

Martin
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20160206/6306538a/attachment-0001.html