[Agda] Q: refinement in emacs

[Christoph Herrmann]

Hi Nils,

> You can use C-c C-s to solve goals which have a /unique/ solution, if
> this solution can be found using unification.


thank you. Agda is able to figure out that b is of type B  given
the equation b = f a.

Best regards

--
  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