The Coq mailing list

[Vadim Zaliva <vzaliva AT cmu.edu>]

On Jan 8, 2015, at 10:21 , Vadim Zaliva <vzaliva AT cmu.edu> wrote:

That leaves me with two approaches:

I turns out I need both approaches.

1. For operators where “o” depends on “i” I used Vop_i {A:Type} (i:nat) : nat -> Type

2. For operators where “i” depends on “o” I used Vop_o {A:Type} (o:nat) : nat -> Type

3. For operators where both “i” and “o” are mutually independent I used Vop_io {A:Type}: nat -> nat-> Type

4. To tie it all together I used Inductive Vop {A:Type} (i o:nat) : Type

Unfortunately even I am not using equalities in type definition I’ve ended up with using “Program” for 

evalVop definition. I am still investigating how it has arisen. But with your help I have certainly already

made a great progress.

Sincerely,
Vadim Zaliva

--

CMU ECE PhD student

Mobile: +1(510)220-1060

Skype: vzaliva