TH1 Type Checking - LF Rules

Rules for Types

   $tType: type
   $i    : $tType
   $o    : $tType
   >     : $tType -> $tType -> $tType     (infix)

Rules for Terms

   $tm   : $tType -> type
   ^     : ($tm A -> $tm B) -> $tm (A > B)
   @     : $tm (A > B) -> $tm A -> $tm B   (infix)

Rules for Term Constructors

\begin{verbatim}
   !     : ($tm A -> $tm $o) -> $tm $o
   ?     : ($tm A -> $tm $o) -> $tm $o
   @+    : ($tm A -> $tm $o) -> $tm A
   @-    : ($tm A -> $tm $o) -> $tm A
   ==    :  $tm A -> $tm A   -> $tm $o

Rules for Proofs

   $istrue : $tm $o -> type

Rules for Polymorphic Constants

   !! : {A: $tType} $tm ((A > $o) > $o)
   ?? : {A: $tType} $tm ((A > $o) > $o)
   @@+: {A: $tType} $tm ((A > $o) > A )
   @@-: {A: $tType} $tm ((A > $o) > A )
   @= : {A: $tType} $tm ( A > A   > $o)