[Agda] Q: refinement in emacs

[Christoph Herrmann]

Hi,

to be precise: I expected that the insertion of f happens automatically
when I started the refinement. It works when I insert f manually.

Is there an example where the refinement gives me some
information that is difficult to figure out myself?

Best regards


On 29 Sep 2009, at 17:06, Christoph Herrmann wrote:

> 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
>
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda

--
  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/ebe3a50c/attachment-0001.html