search

proofpeer / proofpeer-proofscript

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

Incorrect reporting in error messages #23

Closed ghost closed 10 years ago

ghost commented 10 years ago

Given two theories:

theory \Foo extends \root

def foo () = ()

and

theory \Bar extends \Foo

show "hello"
val x = foo 1

proofscript reports a match error in line 3 of file Bar.thy. It should be an error in line 3 of file Foo.thy.