search

Ayertienna / IS5

Intuitionistic S5 logic formalization
4 stars 0 forks source link

Reconsider using inductive definition of subst_t instead of fixpoint for label-free #21

Closed Ayertienna closed 12 years ago

Ayertienna commented 12 years ago

Motivation: right now we have to explicitly state, what is the current context. This becomes much pain in box_LF case, as we have to generate the context manually. With inductive definition we could do the same trick as was used in types_LF, namely to say forall w_fresh \notin L, .

This seems to be useful for proving that subst. order does not matter (we could then prove that the result is the same, not just that regardless of the order of substs. we get terms that have the same type)

Ayertienna commented 12 years ago

Alt: box_LF explicitly stating the name of fresh world it used

Ayertienna commented 12 years ago

Alt': just get rid of current context as a parameter (if this is possible; was possible in subst_t... )

Ayertienna commented 12 years ago

It seems that the last option was easiest to implement. This is now completed.