Hi,<br><br>Relation.Binary.PropositionalEquality exports [_] since library version 0.6. See <a href="http://www.cse.chalmers.se/%7Enad/listings/lib-0.6/Relation.Binary.PropositionalEquality.html#4005" target="_blank">http://www.cse.chalmers.se/~nad/listings/lib-0.6/Relation.Binary.PropositionalEquality.html#4005</a><br>
<br>One solution is to import this module hiding [_]:<br><br>
open import Relation.Binary.PropositionalEquality hiding ([_])<br><br>Cheers,<br>Dan<br><br>(Sorry for double post - sent this from the wrong mail account)<br><br><div class="gmail_quote">On Fri, Mar 30, 2012 at 12:18 PM, Ondrej Rypacek <span dir="ltr"><<a href="mailto:ondrej.rypacek@gmail.com">ondrej.rypacek@gmail.com</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi<br>
<br>
I've downloaded version 2.3.0 of agda , an .6 libraries, and some of<br>
my files have stopped parsing. Namely, I'm getting:<br>
<br>
Don't know how to parse C [ a , b ]. Could mean any one of:<br>
C [ a , b ]<br>
C ([ (a , b) ])<br>
when scope checking C [ a , b ]<br>
<br>
<br>
where _[_,_] is defined as a data constructor<br>
<br>
<br>
My imports are:<br>
<br>
<br>
open import Data.Nat<br>
open import Relation.Binary.PropositionalEquality<br>
<br>
<br>
<br>
I suspect this is a well known or trivial issue , so I'm not attaching<br>
the whole source code.<br>
<br>
Does anyone have an idea, what could be wrong?<br>
<br>
Cheers,<br>
Ondrej<br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
<br>
<br>
</blockquote></div><br>