Re: How do I put proof obs onto operator args?


I am investigating the mailer problem.

LSL 2.3 deals only with total functions, so I don't see any obvious way to
impose the style of proof obligation you are requesting.  (Maybe if I knew
why you wanted to impose it, I could suggest some other way of getting the
same effect.)

We are planning the inclusion of conditional equations in a future version
of LSL.  This would let you say something like

  P(t) :: op(t) == t_set(...);

Then, in order to use the equation to reduce op(t), you would need to prove
P(t).  Is this what you had in mind?

Jim H.