search

proofpeer / proofpeer-proofscript

The language of ProofPeer: ProofScript
MIT License
8 stars 0 forks source link

Have "by" consume everything to the right #56

Closed ghost closed 9 years ago

ghost commented 9 years ago

Currently, to use "by" with a proof procedure given by a complex expession (such as one that takes arguments), we need to surround it with brackets. This is a little ugly:

theorem '∀x. x ∈ two = (x = ∅ ∨ x = one)'
  by (metis [empty,oneDef,two,power,subset,ext])

Can we have it so that the brackets are unnecessary? Thus:

theorem '∀x. x ∈ two = (x = ∅ ∨ x = one)'
  by metis [empty,oneDef,two,power,subset,ext]