[Agda] (s ◃ m ) * (s' ◃ n)

[Andreas Abel]

On 10.01.2014 13:30, Sergei Meshveliani wrote:
> 1) The part
>
>        e
>     where
>     e : ....
>     e =
>
> needs to be skipped (as I usually do), so that the RHS to be just
> (begin ... end).
> But the checker   (MAlonzo of January 8, 2014)
>
> does not allow this, showing      [ lemma s' s 0 m ]   with yellow
> (probably a termination problem).
> So that I have avoided a termination problem by a lucky occasion with
> extra  "e : ...".

Termination errors have red background.  Yellow is for unsolved 
meta-variables.  By giving the type signature for e you probably helped 
Agda to solve some meta-variables.

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/