coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Arbitrary choices for implicit arguments

From: David Leduc <david.leduc6 AT googlemail.com>
To: Coq Club <coq-club AT inria.fr>
Subject: [Coq-Club] Arbitrary choices for implicit arguments
Date: Mon, 20 Sep 2010 03:20:19 +0000
Domainkey-signature: a=rsa-sha1; c=nofws; d=googlemail.com; s=gamma; h=mime-version:date:message-id:subject:from:to:content-type; b=fudVBUSJ/Nb9MhnFP04wOTMiXwEPevEFAs84CYkv8cen7Tyi72tupdnw0pVHItNvfv AE7+eo9lZ51xzf9Q8Yt5kFFg70x6cF5AH+1DxZZ3Enu/xPEm1TlCwHUXPzT9+7XfhH+G GETfkFzqPSzAq6uz5Zr7unxVt78ncy2edFjK0=

Record T : Type := {
carrier : Set ;
op : carrier -> carrier -> carrier
}.

Check fun (t:T)(x y:carrier t), op _ x y.

(*
Above, the implicit argument is inferred to be t.
But there are other legal choices such as below.
On which bases Coq chooses?
*)

Check fun (t:T)(x y:carrier t), op {| carrier := carrier t ; op := fun
x y => x |} x y.

[Coq-Club] Arbitrary choices for implicit arguments, David Leduc