[Agda] I'm not sure... case for the constructor ..., because I get stuck when trying to solve...

[Dmytro Starosud]

Cool, thanks!
I will go this way.

Cheers,
Dmytro


2014-12-06 21:52 GMT+02:00 flicky frans <flickyfrans at gmail.com>:

> Here is one another option:
>
> open import Data.Bool
> open import Relation.Binary.PropositionalEquality
>
> data Term : Bool → Set where
>   I : Term false
>   App : (a b : Bool) → Term a → Term b → Term (a ∨ b)
>
> test' : ∀ {a} → a ≡ false → Term a → Set
> test' p   I                      = Bool
> test' p  (App false false t1 t2) = Bool
> test' () (App false true  t1 t2)
> test' () (App true  b     t1 t2)
>
> test : Term false → Set
> test = test' refl
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20141207/e90d1ac5/attachment-0001.html