coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Variable scope creep?

From: Joachim Breitner <mail AT joachim-breitner.de>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Variable scope creep?
Date: Fri, 10 Nov 2017 18:40:57 -0500
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=mail AT joachim-breitner.de; spf=Neutral smtp.mailfrom=mail AT joachim-breitner.de; spf=None smtp.helo=postmaster AT hermes.serverama.de
Ironport-phdr: 9a23:bIe1kx12I0cyb+FtsmDT+DRfVm0co7zxezQtwd8ZseseLPad9pjvdHbS+e9qxAeQG96Eu7QZ06L/iOPJZy8p2d65qncMcZhBBVcuqP49uEgeOvODElDxN/XwbiY3T4xoXV5h+GynYwAOQJ6tL3DMr2eN7T8OF1C6HEI1Y72tQs+Bx/iwguu14tjYZxhCrDu7e7J7ahus/ivLscxDo4xrIaYwz1PjuHZJZ+Jb3ys8IFuSmz7+4c67/J9mti5KtvM98cNaF6n3KfdrBYdEBSgrZjhmrPbgsgPOGE7WviMR

Hi,

good point. In the real code, however, I have to use {|…|} because it
is a Definition, not an Instance, so I believe I cannot use {…}.

I learned that using Build_ and instantiating the argument works
better:

Class Class f := {
field1 : forall {a}, f a -> unit ;
field2 : forall {a}, f (a -> a) -> unit }.

Definition option_field1 : forall {a}, option a -> unit :=
fun {a} => fun _ => tt.

Definition option_field2 : forall {a}, option (a -> a) -> unit:=
fun {a} => fun _ => tt.

Definition instance1 : Class option :=
Build_Class _ (@option_field1) (@option_field2).

Definition instance2 : Class option :=
Build_Class option (fun {a} => option_field1 )
(@option_field2).

Definition instance3 : Class option :=
Build_Class _ (fun {a} => option_field1 ) (@option_field2).

instance1 and instance2 work, instance3 does not.

Joachim
--
Joachim Breitner

mail AT joachim-breitner.de
http://www.joachim-breitner.de/

Attachment: signature.asc
Description: This is a digitally signed message part

[Coq-Club] Variable scope creep?, Joachim Breitner, 11/09/2017
- Re: [Coq-Club] Variable scope creep?, Yao Li, 11/10/2017
  - Re: [Coq-Club] Variable scope creep?, Joachim Breitner, 11/11/2017
    - Re: [Coq-Club] Variable scope creep?, Gaëtan Gilbert, 11/11/2017