1300

1 
(* Title: HOL/MiniML/MiniML.thy


2 
ID: $Id$


3 
Author: Dieter Nazareth and Tobias Nipkow


4 
Copyright 1995 TU Muenchen


5 


6 
Mini_ML with type inference rules.


7 
*)


8 


9 
MiniML = Type +


10 


11 
(* expressions *)


12 
datatype

1476

13 
expr = Var nat  Abs expr  App expr expr

1300

14 


15 
(* type inference rules *)


16 
consts

1476

17 
has_type :: "(typ list * expr * typ)set"

1300

18 
syntax

1400

19 
"@has_type" :: [typ list, expr, typ] => bool

1525

20 
("((_) / (_) :: (_))" [60,0,60] 60)

1300

21 
translations


22 
"a  e :: t" == "(a,e,t):has_type"


23 


24 
inductive "has_type"


25 
intrs

1476

26 
VarI "[ n < length a ] ==> a  Var n :: nth n a"


27 
AbsI "[ t1#a  e :: t2 ] ==> a  Abs e :: t1 > t2"


28 
AppI "[ a  e1 :: t2 > t1; a  e2 :: t2 ]


29 
==> a  App e1 e2 :: t1"

1300

30 


31 
end


32 
