Hello,
I wanted to ask whether it is somehow possible to restrict the type of a
field inside a record according to values inside of the record itself.
Example:
noeq type theTypeNoRestrictions = {
min: int;
max: int;
func: (int -> Tot int);
}
noeq type theType = {
min: int;
max: int;
func: (x:int{x >= min && x <= max} -> Tot int);
}
If this is not possible yet, are there any alternatives or workarounds?
It doesn't even have to be a record, I only want to access the values of
"min", "max" and be able to call the function "func".
The motivation behind this is, that I want to use elements with a type t
similar to "theType" as a parameter for some functions f. I am currently
using a record because I need access to all the fields of t inside these
functions. Also I want to prove some post-conditions of f, which is why
I need to restrict t.
In reality, the intended type of "func" looks more like this
func: (x:int{x >= min && x <= max} -> Tot (z:int{something z})
but was simplified in the example above because "something z" does not
directly depend on "min" or "max".
I really appreciate any help you can provide.
Regards,
Jannis**
_______________________________________________
fstar-club mailing list
fstar-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/fstar-club
