Subject: Tactics

Keywords: ::tips
          ::proof
          ::usage

Title: override default typing lemma

--------------------------------------------------


To force a STM to be the typing lemma for an ABS,
add a `typing_lemma` property (Object properties) to the STM
with the value being the obid of the ABS.
For Example, length_wf_nat has property:
 typing_lemma:       length
which will cause lemma length_wf_nat to be used as the
typing_lemma for length instead of the expected length_wf.   ⋅
--------------------------------------------------

Authors: NUPRL:t

⋅

Home