Renaming things
There are some names some of us are not happy with. This issue is just meant to track the latest status in these discussions.
-
◇
: After a lot of discussion aboutexcept_last
vs.except_now
, we agreed that depending on whether you look at the adequacy theorem or the state at some point of the proof, either may make sense. We all agreed thatexcept_0
would be acceptable. -
≡
: I still plan to rename this fromuPred_eq
touPred_internal_eq
. - The lowest-level view shift... my latest suggestion was
|=u=> Q update modality
|={E1,E2}=> Q view modality
P ={E1,E2}=> Q view shift
P ={E1,E2}=★ Q linear view shift
or
|=s=> Q state update (modality)
|={E1,E2}=> Q view update (modality)
P ={E1,E2}=> Q view shift
P ={E1,E2}=★ Q linear view shift
I couldn't find JH's last proposal. Robbert expressed that he liked Derek's:
|=p=> Q primitive shift
|={E1,E2}=> Q primitive view shift
P ={E1,E2}=> Q view shift
P ={E1,E2}=★ Q linear view shift
However, my concern here is that it becomes hard to say that we want a "primitive non-view shift". Also, the "primitive view shift" is not primitive...
- Filenames:
base_logic/upred [just the definition, metric space, functors]
base_logic/primitive [primitive connectives and proofs in the model]
base_logic/base_logic or base_logic/logic [upred + primitive + derived connectives/rules]