[Agda] printed goal type

[Sergei Meshveliani]

On Sun, 2015-01-18 at 11:51 -0500, Andrés Sicard-Ramírez wrote:
> 
> 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
> 


Thanks to Andreas and Andrés!
Both variants work. The first I understand as 

   e | yes k≈k' with d ≟n 0 | PE.inspect (_≟n_ d) 0

   ...   | yes d≡0 | PE.[ eq ] =  ⊥-elim $ <→≢ d>0 $ PE.sym d≡0
                                  where
                                  mty-p'ps≡m' : mty (p' ∷ ps) ≡ m'
                                  ...
                                  sm<m' : sm < m'
                                  ... 
                                  d>0 : d > 0
                                  ...
   ...   | no d≢0 | _  with d
   ...                 | suc _ = PE.refl
   ...                 | 0     = ⊥-elim $ d≢0 PE.refl

The second I understand as

   e | yes k≈k'  with m' ∸ m | PE.inspect (_∸_ m') m
 
   ...   | 0     | PE.[ d=0 ] =  ⊥-elim $ <→≢ d>0 $ PE.sym d=0
                                 where 
                                 ... <the same> 
                                 
   ...   | suc _ | _  = PE.refl    -- this avoids the second `with'.


------
Sergei