search

data61 / PSL

Other
65 stars 9 forks source link

SeLFiE: should I pass around Proof.state inside the SeLFiE interpreter? #102

Closed yutakang closed 4 years ago

yutakang commented 5 years ago

Hopefully not. I guess we only have to care about the Proof.state where the proof goal under consideration is declared.

If different Proof.states, such as the Proof.state where certain constants are defined, are necessary in the semantic part of SeLFiE, we have to improve the SeLFiE interpreter.

yutakang commented 4 years ago

Yes. We need it to Dive_In.