[Agda] new generalize feature, first version

[Joachim Breitner]

Hi,


Am Donnerstag, den 29.03.2018, 18:23 +0200 schrieb Nils Anders Danielsson:
> > - What should be the keyword?
> 
> The variant that I have described is similar to sections in Coq. Perhaps
> the following notation (which introduces a block) could be used:
> 
>    section {Γ : Ctxt} … where
> 
> This is similar to "module _ <telescope> where", but with the "drop
> unused bindings" semantics.

a question from the sidelines: There seems to be a crucial difference
to Coq’s section feature, if I am not mistaken: In Coq, you write

   Section Foo.
     Context {x : nat}.
     Definition bar := x + 1.
     Definition baz := bar + 2.
   End Foo.
   Definition foo := bar 1 + 2.

So within the section, x is not generalized, and bar has type nat, but
outside the section, bar has type (nat -> nat).

This forbids calling bar within the Section with a different parameter:

   Section Foo.
     Context {x : nat}.
     Definition bar := x + 1.
     Definition baz := bar 2. (* type error *)
   End Foo.


If I read Peter’s description of his `generalize` feature correctly,
then this generalizes the variables _in each type signature_, and you
can call bar from baz with different arguments for the generalized
parameter.



If I read this correctly, then it would maybe more confusing than
helpful to call it section.

Cheers,
Joachim
-- 
Joachim Breitner
  mail at joachim-breitner.de
  http://www.joachim-breitner.de/
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: This is a digitally signed message part
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180330/fcbbb00e/attachment.sig>