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

[Sergei Meshveliani]

On Fri, 2014-01-10 at 14:13 +0100, Andreas Abel wrote:
> 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.


I tried compilation from the command line, and it reports a termination
check fail
(see my respond to my letter).

In _my_ emacs setting, a  termination check fail  looks as follows:

several calls of the same function are shown _yellow_, and nothing is
reported
(in the case of unsolved meta, it usually reports something).

Concerning emacs:
in command line, I see the reports in full. May be, it is also possible
in emacs -- if I knew how to scroll the lower part, in which the report
is shown. 

Regards,

------
Sergei