The Coq mailing list

[Nikhil Swamy <nswamy AT microsoft.com>]

Hi Coq-club,

Is there some way to construct a coercion in Coq based on the result of a pattern match? Maybe via some use of JMeq?

The example below illustrates what I’d like to accomplish.

 

Many thanks in advance for any pointers,

Nikhil

----

 

Inductive A : Type :=

| One : A

| Two : A.

 

Inductive B : A -> Type := .

 

Definition foo (b: B One) := tt.

 

Definition bar (a:A) (b:B a) : unit :=

  match a with

    | foo b (* some way to coerce b's type to (B One)? *)

    | Two => tt

  end.