The Coq mailing list

[dimitrisg7 <dvekris AT hotmail.com>]

muad wrote:
> 
> 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).
> 
Well, I must prove that a certain transformation from a source language to a
target one preserves the semantics. "data_prop" refers to the type of some
objects the source language has. "data_prop" has the property mentioned
above and I thought that this should be reflected in the initial definition
and not given as a separate hypothesis. What makes things complicated is
function "func", which is actually the order of the type and uses
recursively "data_prop". I would be happy if I could have something like:

Inductive data_prop ...
...
...
with Fixpoint func (data_prop).


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