[Agda] Some proofs by clauses

[Manuel Bärenz]

I didn't try, but how about pattern match on y, for example in a
with-clause? Then the proof should be refl.


On 2017-07-03 15:34, v0id_NULL wrote:
> Dear list,
>
> Help me please. How can I prove type of p2?
>
> module M1 where
>
> open import Data.Nat using (ℕ)
> open import Data.Bool using (Bool; true; false)
> open import Relation.Binary.PropositionalEquality using (_≡_; refl)
>
> f : Bool → Bool → ℕ
> f true x = 1
> f y false = 2
> f false true = 3
>
> p1 : {x : Bool} → f true x ≡ 1
> p1 = refl
>
> p2 : {y : Bool} → f y false ≡ 2
> p2 = {!!}
>
> p3 : f false true ≡ 3
> p3 = 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/20170703/ddc9c05e/attachment.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 819 bytes
Desc: OpenPGP digital signature
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20170703/ddc9c05e/attachment.sig>