On Sun, Dec 13, 2009 at 8:28 AM, Florent Balestrieri <span dir="ltr"><<a href="mailto:fyb@cs.nott.ac.uk">fyb@cs.nott.ac.uk</a>></span> wrote:<br><div class="gmail_quote"><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">
<br>
I'm writing several interdependent modules at once and<br>
because I have priorities, I don't fill every definition :<br>
some are just question marks with which I would deal later.<br>
<br>
Now agda 2.2.4 won't typecheck a module which imports another<br>
uncompleted module, complaining about those unsolved meta<br>
variables. Is there a way to make agda more flexible about<br>
those things?<br>
<br></blockquote><div><br>Maybe there is a better solution, but you can replace those question marks with postulates.<br><br clear="all"></div></div>-- <br>Andrés<br>