[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*To*: Raphael.Couturier@loria.fr*Subject*: Re: Question on operator*From*: R.W.Butler@larc.nasa.gov*Date*: Fri, 10 Apr 1998 11:49:28 -0500 (EST)*Cc*: pvs-help@csl.sri.com*In-Reply-To*: <352E3C44.CE3E7533@loria.fr>*References*: <352E3C44.CE3E7533@loria.fr>*Reply-To*: R.W.Butler@larc.nasa.gov

> I would like to know if another operator exists or if it is possible to > define a new operator having the following behavior. I call op the > operator. > if we want to prove the sequent > A op B > C > --- > D > I should prove the sequents > -- > A > and > B > C > -- > D If you let op be => and use Hide -1 2 on the first subgoal after you issue prop you get what you want. Rick Butler P.S. If you really are free to pick the "op" in a premise, the following might be very productive one: op(a,b: T): bool = FALSE

**References**:**Question on operator***From:*Raphael Couturier <Raphael.Couturier@loria.fr>

- Prev by Date:
**Question on operator** - Next by Date:
**PVS on NT?** - Prev by thread:
**Question on operator** - Next by thread:
**typecheck error** - Index(es):