Closed chaosape closed 6 years ago
It seems that specifications formulas of the form (pi x\ ...) => ... and pi x\ ( ... => ...) are rendered identically.
(pi x\ ...) => ...
pi x\ ( ... => ...)
For a concrete example, consider the Abella commands
Kind t type. Type q t -> o. Theorem test: forall t, { (pi x\q x) => q t } /\ { pi x\(q x => q t)}.
that outputs the following proof state
============================ forall t, {pi x\q x => q t} /\ {pi x\q x => q t}
It seems that specifications formulas of the form
(pi x\ ...) => ...andpi x\ ( ... => ...)are rendered identically.For a concrete example, consider the Abella commands
that outputs the following proof state