[Agda] interactive evaluation and typechecking

[Nils Anders Danielsson]

On 2011-11-14 16:12, Wojciech Jedynak wrote:
> To everybody: Ramana seems not to be the first person to think that _
> should create goals. Is it because is it so in case of Coq (when using
> refine)? I think we should make it more obvious for newcomers to Agda
> that ? should be used.

How? I would expect that every hands-on tutorial explains this. For
instance, the third sentence of

   http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.QuickGuideToEditingTypeCheckingAndCompilingAgdaCode

mentions '?'.

-- 
/NAD