[Agda] Q: refinement in emacs

[Christoph Herrmann]

Hi,

I have doubts that my emacs installation with Agda is working correctly,
so I tried a given example.

I found on one lecture slide of Anton Setzer
CS 336/CS M36 (part 2)/CS M46 Interactive Theorem Proving, Lent Term  
2008, Sec. 3 (c)3-93:

postulate A : Set
postulate B : Set
postulate f : A → B
postulate a : A
b : B
b = {! !}

Then we can insert f into this goal and use menu
Refine (C-c C-r)
The system shows b = f {! !}.
---------------------------------------------------------
Unfortunately, this does not work for me. After loading the file the  
hole is replaced by
b = {   }0
Placing the cursor inside the { } and selecting refinement the  
refinement does not
happen visibly for me, but I'm asked for a number of a goal. I typed 0  
but the goal
did not change to the result as on the slides.

Is there an easy way to check what the reason could be; e.g., the  
values of
environment variables in emacs (I'm using Aquamacs on MacOSX)?

The type inference in simple cases seems to work, although I'm not  
getting
the normal form displayed.

Many thanks in advance
-- 
  Dr. Christoph Herrmann
  University of St Andrews, Scotland/UK
  phone: office: +44 1334 461629, home: +44 1334 478648
  email: ch at cs.st-andrews.ac.uk,  c.herrmann at virgin.net
  URL:   http://www.cs.st-andrews.ac.uk/~ch

  The University of St Andrews is a charity registered in Scotland: No  
SC013532




-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20090929/63805252/attachment.html