search

proofpeer / proofpeer-proofscript

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

Possibly spurious match failures #28

Closed ghost closed 10 years ago

ghost commented 10 years ago

The following snippet fails with "pattern is not a higher-order pattern"

context
  let 'x'
  val foo =
    match term (normalize '(x ↦ x) x')
      case '‹x› = ‹y›' => [x,y]