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

[Andreas Abel]

As always, if you want a more thorough investigation of your case, 
provide self-contained Agda code.

Best,
Andreas

On 10.01.2014 16:36, Sergei Meshveliani wrote:
> 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
>
>


-- 
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/