[Agda] EqReasoning example
Serge D. Mechveliani
mechvel at botik.ru
Mon Mar 4 22:01:46 CET 2013
On Mon, Mar 04, 2013 at 06:24:38PM +0100, Andreas Abel wrote:
> Hello Sergei,
> you are simply using the wrong identifier for the equality chaining.
> The correct one is
> \equiv\< \>
> and you used s.th. like
> \approx( ... )
> First, parentheses () cannot be part of an identifier, since they
> are special symbols in Agda (and any language I know).
Great! It works.
I must have recalled my adventure with \equiv\< $ \>.
My emacs graphics shows very closely the above two kinds of parenthesis.
I rename the chaining one to \equiv[ ], so that it is graphically
More information about the Agda