LF = Pure +

types
  term  context  typing

arities
  term :: logic


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

consts
  Abs           :: "[term, term => term] => term"
  Prod          :: "[term, term => term] => term"

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


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

  star          :: "term"                               ("Type")
  box           :: "term"                               ("Kind")

  "^"           :: "[term, term] => term"               (infixl 20)
  Lam           :: "[idt, term, term] => term"          ("(3Lam _:_. _)" [0, 0, 0] 10)
  Pi            :: "[idt, term, term] => term"          ("(3Pi _:_. _)" [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)"
  "Pi x:A. B"   => "Prod(A, %x. B)"
  "A -> B"      => "Prod(A, _K(B))"
rules
  axiom           "G|- Type:Kind"

  hypothesis      " x:A G|- x:A"

  formation       "[| G |- A:Type; !!x. x:A G |- B(x):S |]==> G |- Prod(A,B):S"

  abstraction     "[| !!x. x:A G |- b(x):B(x);G |- Prod(A,B):S|]==> G |- Abs(A,b):Prod(A,B)" 

  application     "[| G |- F:Prod(A,B); G |- a:A|] ==> G |- F^a : B(a)" 

  weakening "(G |- a:A) ==> x:X G |- a:A" 

end



ML

val print_translation = [("Prod", dependent_tr' ("Pi", "op ->"))];