STT = Pure +

types
  term  context  typing

arities
  term :: logic


syntax
 ""        :: "id => context"                      ("_ ") 
 ""        :: "var => context"                     ("_ ")  

consts
  Abs           :: "[term, term => term] => term"
  Trueprop      :: "[context, typing] => prop"          ("(_ |- _)")


  MT_context    :: "context"                            ("")
  Context       :: "[typing, context] => context"       ("_/ _")

  "^"           :: "[term, term] => term"               (infixl 20)
  Lam           :: "[idt, term, term] => term"          ("(3Lam _:_. _)" [0, 0, 0] 10)
  Has_type      :: "[term, term] => typing"             ("(_:_)" [0, 0] 5)
  "->"          :: "[term, term] => term"               (infixr 10)

translations
  "Lam x:A. B"  == "Abs(A, %x. B)"

rules
  hypothesis      " x:A G|- x:A"
  abstraction     "[| !!x. x:A G |- b(x):B|]==> G |- Abs(A,b):(A -> B)" 
  application     "[| G |- F:(A -> B); G |- a:A|] ==> G |- F^a : B" 
  weakening "(G |- a:A) ==> x:X G |- a:A" 

end