[Agda] printed goal type

[Andrés Sicard-Ramírez]

On 18 January 2015 at 07:11, Sergei Meshveliani <mechvel at botik.ru> wrote:

> Please,
> how to fix the attached program?
> (about 100 lines).
>
> It ends with
>
>   e | yes k≡k'  with d
>   e | yes k≡k' | suc _ =  PE.refl
>   e | yes k≡k' | 0     =  ⊥-elim $ <→≢ d>0 $ PE.sym d≡0
>                           where
>                           ...
>                           d>0 : d > 0
>                           d>0 = m<n→n∸m>0 m<m'
>
>                           d≡0 : d ≡ 0
>                           d≡0 = ?
>

As Andreas said, you need to use the inspect pattern.

You can replace

  e | yes k≡k' with d

with

  e | yes k≡k' with m' ∸ m | inspect (_∸_ m') m

-- 
Andrés
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20150118/b35c014c/attachment-0001.html