On Mon, May 21, 2012 at 3:29 AM, Lu Zhao luz...@cs.utah.edu wrote:
This is particularly dangerous when I have proof automation scripts that
try different rewriting rules. The number reported is not representative
on the complexity of the problem, but the number of inference steps
conducted by
Ramana Kumar wrote:
On Mon, May 21, 2012 at 3:29 AM, Lu Zhao luz...@cs.utah.edu wrote:
This is particularly dangerous when I have proof automation scripts that
try different rewriting rules. The number reported is not representative
on the complexity of the problem, but the number of
Hi Bill,
| Thanks, John! Yet again you were extremely helpful. Your fix works:
|
| let plane = new_definition
| `plane S Between Equiv =
| (Between SUBSET {(x,y,z) | x IN S /\ y IN S /\ z IN S} /\
| Equiv SUBSET {(x,y,z,w) | x IN S /\ y IN S /\ z IN S /\ w IN S})`;;
Yes, that seems to be
First of all, there is the issue of currying versus uncurrying
again: if you want to write Twiddle(A, l, B) then you need to make
the type of Twiddle `:point#line#point-bool`, or if you want to
keep the type as ``:point-line-point-bool` you need to write
`Twiddle A l B`. Also, if
