Skip to content
  • Robbert Krebbers's avatar
    Make specialization patterns for persistent premises more uniform. · 65bfa071
    Robbert Krebbers authored
    Changes:
    - We no longer have a different syntax for specializing a term H : P -★ Q whose
      range P or domain Q is persistent. There is just one syntax, and the system
      automatically determines whether either P or Q is persistent.
    - While specializing a term, always modalities are automatically stripped. This
      gets rid of the specialization pattern !.
    - Make the syntax of specialization patterns more consistent. The syntax for
      generating a goal is [goal_spec] where goal_spec is one of the following:
    
        H1 .. Hn : generate a goal using hypotheses H1 .. Hn
       -H1 .. Hn : generate a goal using all hypotheses but H1 .. Hn
               # : generate a goal for the premise in which all hypotheses can be
                   used. This is only allowed when specializing H : P -★ Q where
                   either P or Q is persistent.
               % : generate a goal for a pure premise.
    65bfa071