coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Gabriel Scherer <gabriel.scherer AT gmail.com>
- To: Coq Club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] Trouble with coercions
- Date: Sat, 27 Sep 2014 19:18:30 +0200
Situation (1) (coercion from n to n+1) works by just declaring the coercion as the manual says:
http://coq.inria.fr/coq/refman/Reference-Manual021.html
Coercion promote : term >-> term.http://coq.inria.fr/coq/refman/Reference-Manual021.html
Check (makeTuple 1 c x). (* 0->1: ok *)
Check (makeTuple 2 x x). (* 1->2: ok *)
Check (makeTuple 2 c x). (* 0->2: fails *)
On Sat, Sep 27, 2014 at 6:48 PM, Anders Lundstedt <anders AT anderslundstedt.se> wrote:
Here is another example, which I think is closely related to my
problem (1). http://pastebin.com/CWwWvPRu
Parameter A : nat -> Type.
SubClass A0 := A 0.
SubClass A1 := A 1.
Parameter A0toA1 :> A0 -> A1.
Print Graph.
(* we now have coercions A0,A1 >-> A and A0 >-> A1 *)
Parameter (a0 : A 0) (a1 : A 1).
Parameter (a0' : A0) (a1' : A1).
Parameter f : A 1 -> Type.
Parameter f' : A1 -> Type.
(* term of type A0 when term of type A1 expected: *)
Check (f' a0'). (* OK *)
(* possible to avoid casts below, e.g. get "f a0'" to typecheck? *)
(* term of type A0 when type of A 1 expected: *)
Check (f (a0' : A1)).
(* term of type A 0 when term of type A1 expected: *)
Check (f' (a0 : A0)).
(* term of type A 0 when term of type A 1 expected: *)
Check (f ((a0 : A0) : A1)). (* note: double cast needed! *)
- [Coq-Club] Trouble with coercions, Anders Lundstedt, 09/26/2014
- Re: [Coq-Club] Trouble with coercions, Anders Lundstedt, 09/27/2014
- Re: [Coq-Club] Trouble with coercions, Gabriel Scherer, 09/27/2014
- Re: [Coq-Club] Trouble with coercions, Anders Lundstedt, 09/27/2014
Archive powered by MHonArc 2.6.18.