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

Definition weq 38
Description: The equality function has type al -> al -> *, i.e. it is polymorphic over all types, but the left and right type must agree.
Assertion
Ref Expression
weq |- = :(al -> (al -> *))

Detailed syntax breakdown of Definition weq
StepHypRef Expression
1 hal . . 3 type al
2 hb 3 . . . 4 type *
31, 2ht 2 . . 3 type (al -> *)
41, 3ht 2 . 2 type (al -> (al -> *))
5 ke 7 . 2 term =
64, 5wffMMJ2t 12 1 wff = :(al -> (al -> *))
Colors of variables: type var term
This definition is referenced by:  wtru  40  eqcomx  47  weqi  68  eqcomi  70  mpbi  72  eqid  73  ded  74  ceq12  78  leq  81  beta  82  distrc  83  distrl  84  eqtri  85  oveq123  88  hbov  101  clf  105  ovl  107  alval  132  euval  134  imval  136  anval  138  eta  166  cbvf  167  leqf  169  ax10  200  axrep  207
  Copyright terms: Public domain W3C validator