The Coq mailing list

[muad <muad.dib.space AT gmail.com>]

Hi dimitry,

Inductive data_prop2 (m : nat) : nat -> Set :=
| dp2_nil : data_prop2 m 0
| dp2_consX : forall el i, func el = m -> data_prop2 m i -> data_prop2 m (S
i). 

Inductive data_prop (m : nat) : nat -> Set :=
| dp_nil : data_prop m 0
| dp_cons : forall el i, func el < m -> data_prop m i -> data_prop m (S i)
| dp_consX : forall el i, func el = m -> data_prop2 m i -> data_prop m (S
i).

May be a better way to phrase it, since data_prop2 isn't mutual. What sort
of properties to do you expect of this though, and what proofs do you want
want to make? (I could not suggest something without knowing what you are
doing, in a bit more detail).


-- 
View this message in context: 
http://www.nabble.com/Data-Structures-tp22535211p22541191.html
Sent from the Coq mailing list archive at Nabble.com.