HOLE Home Higher-Order Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  HOLE Home  >  Th. List  >  wl Structured version   Unicode version

Definition wl 59
Description: The type of a lambda abstraction.
Hypothesis
Ref Expression
wl.1 |- T:be
Assertion
Ref Expression
wl |- \x:al T:(al -> be)

Detailed syntax breakdown of Definition wl
StepHypRef Expression
1 hal . . 3 type al
2 hbe . . 3 type be
31, 2ht 2 . 2 type (al -> be)
4 vx . . 3 var x
5 tt . . 3 term T
61, 4, 5kl 6 . 2 term \x:al T
73, 6wffMMJ2t 12 1 wff \x:al T:(al -> be)
Colors of variables: type var term
This definition is referenced by:  leq  81  beta  82  distrc  83  distrl  84  hbxfrf  97  hbc  100  hbl  102  clf  105  ovl  107  wal  124  wfal  125  wan  126  wim  127  wnot  128  wex  129  wor  130  weu  131  alval  132  exval  133  euval  134  orval  137  anval  138  ax4  140  alrimiv  141  cla4v  142  dfan2  144  olc  154  orc  155  exlimdv2  156  exlimdv  157  ax4e  158  cla4ev  159  19.8a  160  eta  166  cbvf  167  leqf  169  alrimi  170  exlimd  171  alimdv  172  eximdv  173  alnex  174  exnal1  175  ac  184  exmid  186  exnal  188  ax5  194  ax6  195  ax7  196  ax9  199  ax10  200  ax11  201  ax12  202  axext  206  axrep  207  axpow  208  axun  209
  Copyright terms: Public domain W3C validator