matita/matita/contribs/lambda_delta/Basic_2/reducibility/twhnf.ma

   1 include "Basic_2/reducibility/tpr.ma".
   2
   3 (* CONTEXT-FREE WEAK HEAD NORMAL TERMS **************************************)
   4
   5 definition twhnf: term → Prop ≝
   6    NF … tpr (thom …).
   7
   8 interpretation
   9    "context-free weak head normality (term)"
  10    'WHdNormal T = (twhnf T).
  11
  12 (* Basic properties *********************************************************)