How do I put proof obs onto operator args?
Subject: How do I put proof obs onto operator args?
From: kirk@zipcode.Jpl.Nasa.Gov (Kirk Reinholtz)
Date: Tue, 08 Mar 94 11:55:50 -0800
Delivery-Date: Tue, 08 Mar 94 11:57:18 -0800
[Forwarded by firstname.lastname@example.org for kirk@zipcode.Jpl.Nasa.Gov]
Say I have something like
T tuple of a:A, b:B;
op(t) == t_set(...);
But I want all uses of op() to incur a proof obligation that
some predicates on T hold (e.g. b has certain properties, or
Am I going about this all wrong, or is there a way to state this,
or is there a better paradigm, or what?
Thanks to all who read this!