Combine does not beta-reduce its first argument

proofpeer / proofpeer-proofscript

The language of ProofPeer: ProofScript

MIT License

8 stars 0 forks source link

Combine does not beta-reduce its first argument #26

Closed ghost closed 10 years ago

ghost commented 10 years ago

The following snippet fails with "dest_equals: term is not an equality".

theory \Bugs extends \root

context
  let 'x : ℙ'
  let 'f : ℙ → ℙ'
  assume foo:'(x ↦ f = f) x'
  val bar = combine (foo,reflexive 'x')

phlegmaticprogrammer commented 10 years ago

The general issue here seems to be that if kernel methods demand a certain shape for theorem or term parameters, and this shape can be described as a higher-order pattern, then the kernel must use higher-order pattern matching instead of simple structural pattern matching to destruct those parameters.