search

data61 / PSL

Other
65 stars 9 forks source link

SeLFiE: move Is_Rule_Of_Node from Eval_Node to Eval_Path #122

Closed yutakang closed 4 years ago

yutakang commented 4 years ago

Probably it would be cleaner if we do not have anything related to Proof.context in Eval_Node.

yutakang commented 4 years ago

No... it is alright to keep Is_Rule_Of_Node in Eval_Node since it is a test about a property of node rather than a property of a path.

Instead, we should move Unode_Has_Print from Eval_Path to Eval_Unode.

yutakang commented 4 years ago

Is_Rule_Of_Print of string * string in https://github.com/data61/PSL/blob/f0227fe15e9f3d0986d8210b2b4e26f3e2519603/SeLFiE/Eval_Print.ML#L17