conversions should return theorems in current context

phlegmaticprogrammer commented 8 years ago

I've changed the absConv definition to look like this:

def absConv conv =
  tm =>
    match destabs tm
      case [ctx,_,bod] =>
        match incontext<ctx> conv bod
          case nil => nil
          case th => 
            th = incontext<ctx> lift th
            abstract (lift! th)
      case _ => nil

Note that compared to the paper, I had to insert the line th = incontext<ctx> lift th, because conversions don't currently obey the contract to return theorems in the current context they are called in. I think this invariant should be introduced, and then that line I inserted can be dropped.

ghost commented 8 years ago

I'm not really clear on what I am supposed to do here. The only conversion which messes with context is absConv.

Are we meeting today, btw?

Steven Obua notifications@github.com writes:

Assigned #76 to @Chattered.

Reply to this email directly or view it on GitHub: https://github.com/proofpeer/proofpeer-proofscript/issues/76#event-584961568

Sent with my mu4e

pikan commented 8 years ago

I have us down for our usual noon meeting. So, let's meet.

Jacques

On 11 March 2016 at 10:16, Phil Scott notifications@github.com wrote:

I'm not really clear on what I am supposed to do here. The only conversion which messes with context is absConv.

Are we meeting today, btw?

Steven Obua notifications@github.com writes:

Assigned #76 to @Chattered.

Reply to this email directly or view it on GitHub:

https://github.com/proofpeer/proofpeer-proofscript/issues/76#event-584961568

Sent with my mu4e

— Reply to this email directly or view it on GitHub https://github.com/proofpeer/proofpeer-proofscript/issues/76#issuecomment-195307872 .

phlegmaticprogrammer commented 8 years ago

Am coming for the meet, too.

Somehow there must be another conversion which does not return the theorem in the context in which it is called (which is the invariant on conversions I am proposing). That might even be due to ProofScript not behaving as we would expect it to do in some situations. Any idea which conversion could be responsible for that?

On Fri, Mar 11, 2016 at 10:16 AM, Phil Scott notifications@github.com wrote:

I'm not really clear on what I am supposed to do here. The only conversion which messes with context is absConv.

Are we meeting today, btw?

Steven Obua notifications@github.com writes:

Assigned #76 to @Chattered.

Reply to this email directly or view it on GitHub:

https://github.com/proofpeer/proofpeer-proofscript/issues/76#event-584961568

Sent with my mu4e

— Reply to this email directly or view it on GitHub https://github.com/proofpeer/proofpeer-proofscript/issues/76#issuecomment-195307872 .

Steven Obua School of Informatics, University of Edinburgh

Join us at proofpeer.net and revolutionise math, engineering and the sciences! http://proofpeer.net

proofpeer / proofpeer-proofscript

conversions should return theorems in current context #76