coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Implicit generalization w/ Context

From: Erkki Luuk <erkkil AT gmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] Implicit generalization w/ Context
Date: Thu, 26 Oct 2017 01:51:03 +0300
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=erkkil AT gmail.com; spf=Pass smtp.mailfrom=erkkil AT gmail.com; spf=None smtp.helo=postmaster AT mail-it0-f48.google.com
Ironport-phdr: 9a23:dNSk8BMrsjKPIHMr4gkl6mtUPXoX/o7sNwtQ0KIMzox0K/n7rarrMEGX3/hxlliBBdydsK0UzbeO+4nbGkU+or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6a8TWO6msZHQy6Pg5oLMz0HJTThoK5zbOc4ZrWNihShzm8KZdvMRb++QjLtcoXhaNtL68wzl3CpX4eKLce/n9hOV/Gx0W03cy35pM2qyk=

Hi all

I have 3 questions about implicit generalization w/ Context (below is a minimal ex.):

Context `(b:bool)`{c:bool}.

Parameter g: forall {x y:bool}, Prop.

Check @g b c: Prop.

1. Is there a difference between Context `(b:bool) and Context `{b:bool}?

2. Is it possible to declare implicitly generalizable variables w/out specifying types for each of them separately? Something like `(b c:bool) (which seems to be treated as an application).

3. Can I give a single declaration for a set of implicitly generalizable variables x..., where ... is a number or a (number of) '(-s)? (Or indeed, for any set of variables w/ such specification)

Best wishes

Erkki

[Coq-Club] Implicit generalization w/ Context, Erkki Luuk, 10/26/2017