[Agda] new generalize feature, first version

Nils Anders Danielsson nad at cse.gu.se
Sun Apr 1 21:38:28 CEST 2018


On 2018-04-01 20:04, Peter Divianszky wrote:
> Yes, it seems that Coq also has a forall-generalisation. The main
> difference is that it is not possible to specify the types of the
> variables to be generalized.

Correct me if I'm wrong, but I don't think Coq has a first-class
implicit function space like Agda does. (This function space has led to
a number of problems.)

-- 
/NAD


More information about the Agda mailing list