Set Implicit Arguments.
Require Export LibCore DeepSyntax.
Coercion trm_val : val >-> trm.
Coercion trm_var : var >-> trm.
Coercion pat_var : var >-> pat.
Coercion val_int : int >-> val.
Coercion val_nat (x:nat) := val_int (x:int).
Coercion _Bool : bool >-> val.
Coercion _Unit : unit >-> val.
Definition newscope := True.
Notation "'__trm_scope_init__'" := newscope : trm_scope.
Notation "'__val_scope_init__'" := newscope : val_scope.
Notation "'__pat_scope_init__'" := newscope : pat_scope.
Open Scope pat_scope.
Open Scope val_scope.
Open Scope trm_scope.
Delimit Scope trm_scope with trm.
Delimit Scope val_scope with val.
Delimit Scope pat_scope with pat.
Bind Scope trm_scope with trm.
Bind Scope val_scope with val.
Bind Scope pat_scope with pat.
Open Scope var_scope.
Delimit Scope var_scope with var.
Bind Scope var_scope with var.
Arguments Scope trm_val [ val_scope ].
Arguments Scope trm_exn [ val_scope ].
Arguments Scope trm_app [ trm_scope trm_scope ].
Arguments Scope trm_try [ trm_scope trm_scope ].
Arguments Scope trm_fix [ var_scope pat_scope trm_scope trm_scope ].
Arguments Scope val_fix [ var_scope pat_scope trm_scope trm_scope ].
Arguments Scope trm_con [ _ trm_scope ].
Arguments Scope val_con [ _ val_scope ].
Arguments Scope pat_con [ _ pat_scope ].
Arguments Scope pat_con [ var_scope pat_scope ].
Arguments Scope pat_var [ var_scope ].
Arguments Scope trm_var [ var_scope ].
Notation "'\' v" := (trm_val v)
(at level 28) : trm_scope.
Notation "t1 ' t2" := (trm_app t1 t2)
(at level 29, left associativity) : trm_scope.
Notation "'exn' v" := (trm_exn v)
(at level 29) : trm_scope.
Notation "'Exn' c" := (exn (val_con c nil))
(at level 29) : trm_scope.
Notation "''raise'" := (\ val_builtin builtin_throw)
(at level 0) : trm_scope.
Notation "''throw' t" := ('raise ' t)
(at level 29) : trm_scope.
Notation "''Throw' c" := ('throw (Exn c))
(at level 29) : trm_scope.
Notation "''crash'" := ('Throw con_match_failure)
(at level 0) : trm_scope.
Notation "''fail'" := ('Throw con_user_failure)
(at level 0) : trm_scope.
Notation "c '#'" := (pat_con c nil)
(at level 27, format "c #") : pat_scope.
Notation "c '#' '(' x1 ')'" := (pat_con c ((x1%pat)::(@nil pat)))
(at level 27, format "c # ( x1 )") : pat_scope.
Notation "c '#' '(' x1 ',' x2 ')'" := (pat_con c ((x1%pat)::(x2%pat)::(@nil pat)))
(at level 27, format "c # ( x1 , x2 )") : pat_scope.
Notation "c '#' '(' x1 ',' x2 ',' x3 ')'" := (pat_con c ((x1%pat)::(x2%pat)::(x3%pat)::(@nil pat)))
(at level 27, format "c # ( x1 , x2 , x3 )") : pat_scope.
Notation "c '#'" := (trm_con c nil)
(at level 27, format "c #") : trm_scope.
Notation "c '#' '(' x1 ')'" := (trm_con c ((x1%trm)::(@nil trm)))
(at level 27, format "c # ( x1 )") : trm_scope.
Notation "c '#' '(' x1 ',' x2 ')'" := (trm_con c ((x1%trm)::(x2%trm)::(@nil trm)))
(at level 27, format "c # ( x1 , x2 )") : trm_scope.
Notation "c '#' '(' x1 ',' x2 ',' x3 ')'" := (trm_con c ((x1%trm)::(x2%trm)::(x3%trm)::(@nil trm)))
(at level 27, format "c # ( x1 , x2 , x3 )") : trm_scope.
Notation "c '#'" := (val_con c nil)
(at level 27, format "c #").
Notation "c '#' '(' x1 ')'" := (val_con c ((x1%val)::(@nil val)))
(at level 27, format "c # ( x1 )") : val_scope.
Notation "c '#' '(' x1 ',' x2 ')'" := (val_con c ((x1%val)::(x2%val)::(@nil val)))
(at level 27, format "c # ( x1 , x2 )") : val_scope.
Notation "c '#' '(' x1 ',' x2 ',' x3 ')'" := (val_con c ((x1%val)::(x2%val)::(x3%val)::(@nil val)))
(at level 27, format "c # ( x1 , x2 , x3 )") : val_scope.
Notation "c '##' vs '++' t '++' ts" :=
(trm_con c ((LibList.map trm_val vs) ++ t::ts))
(at level 28, vs at level 0, t at level 0, ts at level 0,
format "c '##' vs '++' t '++' ts") : trm_scope.
Notation "'pat_tuple' xs" := (pat_con con_tuple xs)
(at level 29, only parsing) : pat_scope.
Notation "'trm_tuple' xs" := (trm_con con_tuple xs)
(at level 29, only parsing) : trm_scope.
Notation "'val_tuple' xs" := (val_con con_tuple xs)
(at level 29, only parsing) : val_scope.
Notation "'#'" := (pat_tuple nil)
(at level 28) : pat_scope.
Notation "'#' '(' x1 ')'" := (pat_tuple ((x1%pat)::(@nil pat)))
(at level 28, format "# '(' x1 ')'") : pat_scope.
Notation "'#' '(' x1 ',' x2 ')'" := (pat_tuple ((x1%pat)::(x2%pat)::(@nil pat)))
(at level 28, format "# ( x1 , x2 )") : pat_scope.
Notation "'#' '(' x1 ',' x2 ',' x3 ')'" := (pat_tuple ((x1%pat)::(x2%pat)::(x3%pat)::(@nil pat)))
(at level 28, format "# ( x1 , x2 , x3 )") : pat_scope.
Notation "'#'" := (trm_tuple nil)
(at level 28) : trm_scope.
Notation "'#' '(' x1 ')'" := (trm_tuple ((x1%trm)::(@nil trm)))
(at level 28, format "# '(' x1 ')'") : trm_scope.
Notation "'#' '(' x1 ',' x2 ')'" := (trm_tuple ((x1%trm)::(x2%trm)::(@nil trm)))
(at level 28, format "# ( x1 , x2 )") : trm_scope.
Notation "'#' '(' x1 ',' x2 ',' x3 ')'" := (trm_tuple ((x1%trm)::(x2%trm)::(x3%trm)::(@nil trm)))
(at level 28, format "# ( x1 , x2 , x3 )") : trm_scope.
Notation "'#'" := (val_tuple nil)
(at level 28) : val_scope.
Notation "'#' '(' x1 ')'" := (val_tuple ((x1%val)::(@nil val)))
(at level 28, format "# '(' x1 ')'") : val_scope.
Notation "'#' '(' x1 ',' x2 ')'" := (val_tuple ((x1%val)::(x2%val)::(@nil val)))
(at level 28, format "# ( x1 , x2 )") : val_scope.
Notation "'#' '(' x1 ',' x2 ',' x3 ')'" := (val_tuple ((x1%val)::(x2%val)::(x3%val)::(@nil val)))
(at level 28, format "# ( x1 , x2 , x3 )") : val_scope.
Notation "c '#'" := (pat_con c nil)
(at level 27, format "c #") : pat_scope.
Notation "c '#' '(' x1 ')'" := (pat_con c ((x1:pat)::nil))
(at level 27, format "c # ( x1 )") : pat_scope.
Notation "c '#' '(' x1 ',' x2 ')'" := (pat_con c ((x1:pat)::(x2:pat)::nil))
(at level 27, format "c # ( x1 , x2 )") : pat_scope.
Notation "c '#' '(' x1 ',' x2 ',' x3 ')'" := (pat_con c ((x1:pat)::(x2:pat)::(x3:pat)::nil))
(at level 27, format "c # ( x1 , x2 , x3 )") : pat_scope.
Notation "c '#'" := (trm_con c nil)
(at level 27, format "c #") : trm_scope.
Notation "c '#' '(' x1 ')'" := (trm_con c ((x1:trm)::nil))
(at level 27, format "c # ( x1 )") : trm_scope.
Notation "c '#' '(' x1 ',' x2 ')'" := (trm_con c ((x1:trm)::(x2:trm)::nil))
(at level 27, format "c # ( x1 , x2 )") : trm_scope.
Notation "c '#' '(' x1 ',' x2 ',' x3 ')'" := (trm_con c ((x1:trm)::(x2:trm)::(x3:trm)::nil))
(at level 27, format "c # ( x1 , x2 , x3 )") : trm_scope.
Notation "c '#'" := (val_con c nil)
(at level 27, format "c #") : val_scope.
Notation "c '#' '(' x1 ')'" := (val_con c ((x1:val)::nil))
(at level 27, format "c # ( x1 )") : val_scope.
Notation "c '#' '(' x1 ',' x2 ')'" := (val_con c ((x1:val)::(x2:val)::nil))
(at level 27, format "c # ( x1 , x2 )") : val_scope.
Notation "c '#' '(' x1 ',' x2 ',' x3 ')'" := (val_con c ((x1:val)::(x2:val)::(x3:val)::nil))
(at level 27, format "c # ( x1 , x2 , x3 )") : val_scope.
Notation "'pat_tuple' xs" := (pat_con con_tuple xs)
(at level 29, only parsing) : pat_scope.
Notation "'trm_tuple' xs" := (trm_con con_tuple xs)
(at level 29, only parsing) : trm_scope.
Notation "'val_tuple' xs" := (val_con con_tuple xs)
(at level 29, only parsing) : val_scope.
Notation "'#'" := (pat_tuple nil)
(at level 28) : pat_scope.
Notation "'#' '(' x1 ')'" := (pat_tuple ((x1:pat)::nil))
(at level 28, format "# '(' x1 ')'") : pat_scope.
Notation "'#' '(' x1 ',' x2 ')'" := (pat_tuple ((x1:pat)::(x2:pat)::nil))
(at level 28, format "# ( x1 , x2 )") : pat_scope.
Notation "'#' '(' x1 ',' x2 ',' x3 ')'" := (pat_tuple ((x1:pat)::(x2:pat)::(x3:pat)::nil))
(at level 28, format "# ( x1 , x2 , x3 )") : pat_scope.
Notation "'#'" := (trm_tuple nil)
(at level 28) : trm_scope.
Notation "'#' '(' x1 ')'" := (trm_tuple ((x1:trm)::nil))
(at level 28, format "# '(' x1 ')'") : trm_scope.
Notation "'#' '(' x1 ',' x2 ')'" := (trm_tuple ((x1:trm)::(x2:trm)::nil))
(at level 28, format "# ( x1 , x2 )") : trm_scope.
Notation "'#' '(' x1 ',' x2 ',' x3 ')'" := (trm_tuple ((x1:trm)::(x2:trm)::(x3:trm)::nil))
(at level 28, format "# ( x1 , x2 , x3 )") : trm_scope.
Notation "'#'" := (val_tuple nil)
(at level 28) : val_scope.
Notation "'#' '(' x1 ')'" := (val_tuple ((x1:val)::nil))
(at level 28, format "# '(' x1 ')'") : val_scope.
Notation "'#' '(' x1 ',' x2 ')'" := (val_tuple ((x1:val)::(x2:val)::nil))
(at level 28, format "# ( x1 , x2 )") : val_scope.
Notation "'#' '(' x1 ',' x2 ',' x3 ')'" := (val_tuple ((x1:val)::(x2:val)::(x3:val)::nil))
(at level 28, format "# ( x1 , x2 , x3 )") : val_scope.
Notation "''fun' p1 ''->' t" :=
(trm_fix novar p1 t 'crash)
(at level 200, p1 at level 0) : trm_scope.
Notation "''fun' p1 p2 '-> t" :=
('fun p1 '-> 'fun p2 '-> t)
(at level 200, p1 at level 0, p2 at level 0) : trm_scope.
Notation "''fun' p1 p2 p3 '-> t" :=
('fun p1 '-> 'fun p2 p3 '-> t)
(at level 200, p1 at level 0, p2 at level 0,
p3 at level 0) : trm_scope.
Notation "''fun' p1 p2 p3 p4 '-> t" :=
('fun p1 '-> 'fun p2 p3 p4 '-> t)
(at level 200, p1 at level 0, p2 at level 0, p3 at level 0,
p4 at level 0) : trm_scope.
Notation "''fun' p1 p2 p3 p4 p5 '-> t" :=
('fun p1 '-> 'fun p2 p3 p4 p5 '-> t)
(at level 200, p1 at level 0, p2 at level 0, p3 at level 0,
p4 at level 0, p5 at level 0) : trm_scope.
Notation "''function' '| p1 '-> t1" :=
('fun p1 '-> t1)
(at level 200, only parsing) : trm_scope.
Notation "''function' ''|' p1 ''->' t1 ''|' p2 ''->' t2" :=
(trm_fix novar p1 t1 ('fun p2 '-> t2))
(at level 200) : trm_scope.
Notation "''function' '| p1 '-> t1 '| p2 '-> t2 '| p3 '-> t3" :=
(trm_fix novar p1 t1 ('function '| p2 '-> t2 '| p3 '-> t3))
(at level 200) : trm_scope.
Notation "''function' '| p1 '-> t1 '| p2 '-> t2 '| p3 '-> t3 '| p4 '-> t4" :=
(trm_fix novar p1 t1 ('function '| p2 '-> t2 '| p3 '-> t3 '| p4 '-> t4))
(at level 200) : trm_scope.
Notation "''function' '| p1 '-> t1 '| p2 '-> t2 '| p3 '-> t3 '| p4 '-> t4 '| p5 '-> t5" :=
(trm_fix novar p1 t1 ('function '| p2 '-> t2 '| p3 '-> t3 '| p4 '-> t4 '| p5 '-> t5))
(at level 200) : trm_scope.
Notation "''match' t ''with' '| p1 '-> t1" :=
(('function '| p1%pat '-> t1) ' t)
(at level 200) : trm_scope.
Notation "''match' t ''with' '| p1 '-> t1 '| p2 '-> t2" :=
(('function '| p1%pat '-> t1 '| p2%pat '-> t2) ' t)
(at level 200) : trm_scope.
Notation "''match' t ''with' '| p1 '-> t1 '| p2 '-> t2 '| p3 '-> t3" :=
(('function '| p1%pat '-> t1 '| p2%pat '-> t2 '| p3%pat '-> t3) ' t)
(at level 200) : trm_scope.
Notation "''match' t ''with' '| p1 '-> t1 '| p2 '-> t2 '| p3 '-> t3 '| p4 '-> t4" :=
(('function '| p1%pat '-> t1 '| p2%pat '-> t2 '| p3%pat '-> t3 '| p4%pat '-> t4) ' t)
(at level 200) : trm_scope.
Notation "''match' t ''with' '| p1 '-> t1 '| p2 '-> t2 '| p3 '-> t3 '| p4 '-> t4 '| p5 '-> t5" :=
(('function '| p1%pat '-> t1 '| p2%pat '-> t2 '| p3%pat '-> t3 '| p4%pat '-> t4 '| p5%pat '-> t5) ' t)
(at level 200) : trm_scope.
Notation "''try' t1 ''catch' t2" := (trm_try t1 t2)
(at level 60) : trm_scope.
Notation "''try' t ''with' '| p1 '-> t1 'end" :=
(trm_try t ('function '| p1 '-> t1))
(at level 60) : trm_scope.
Notation "''try' t ''with' '| p1 '-> t1 '| p2 '-> t2 'end" :=
(trm_try t ('function '| p1 '-> t1 '| p2 '-> t2))
(at level 60) : trm_scope.
Notation "''Match_failure'" := (con_match_failure) (at level 0).
Notation "''Div_by_zero'" := (con_div_by_zero) (at level 0).
Notation "''Not_found'" := (con_not_found) (at level 0).
Notation "''match_failure'" := (val_con con_match_failure nil)
(at level 0) : val_scope.
Notation "''div_by_zero'" := (val_con con_div_by_zero nil)
(at level 0) : val_scope.
Notation "''not_found'" := (val_con con_not_found nil)
(at level 0) : val_scope.
Notation "''let' p '= t1 ''in' t2" :=
(('fun p '-> t2) ' t1)
(at level 200, p at level 0) : trm_scope.
Notation "''let' f p1 '= t1 ''in' t2" :=
('let f '= ('fun p1 '-> t1) 'in t2)
(at level 200, f at level 0, p1 at level 0) : trm_scope.
Notation "''let' f p1 p2 '= t1 ''in' t2" :=
('let f '= ('fun p1 p2 '-> t1) 'in t2)
(at level 200, f at level 0, p1 at level 0,
p2 at level 0) : trm_scope.
Notation "''let' f p1 p2 p3 '= t1 ''in' t2" :=
('let f '= ('fun p1 p2 p3 '-> t1) 'in t2)
(at level 200, f at level 0, p1 at level 0,
p2 at level 0) : trm_scope.
Notation "''let_rec_fun' f '= ''fun' p1 '-> t ''in' e" :=
('let (pat_var f) '= (trm_fix f p1 t 'crash) 'in e)
(at level 200, f at level 0, p1 at level 0) : trm_scope.
Notation "''let_rec_fun' f '= ''fun' p1 '-> ''fun' p2 '-> t ''in' e" :=
('let (pat_var f) '= (trm_fix f p1 ('fun p2 '-> t) 'crash) 'in e)
(at level 200, f at level 0, p1 at level 0, p2 at level 0) : trm_scope.
Notation "''let_rec_fun' f '= ''fun' p1 '-> ''fun' p2 '-> ''fun' p3 '-> t ''in' e" :=
('let (pat_var f) '= (trm_fix f p1 ('fun p2 p3 '-> t) 'crash) 'in e)
(at level 200, f at level 0, p1 at level 0, p2 at level 0, p3 at level 0) : trm_scope.
Notation "''let_rec_fun' f '= ''fun' p1 '-> ''fun' p2 '-> ''fun' p3 '-> ''fun' p4 '-> t ''in' e" :=
('let (pat_var f) '= (trm_fix f p1 ('fun p2 p3 p4 '-> t) 'crash) 'in e)
(at level 200, f at level 0, p1 at level 0, p2 at level 0, p3 at level 0, p4 at level 0) : trm_scope.
Notation "''let_rec_function' f '= ''function' '| p1 '-> t1 ''in' e" :=
('let (pat_var f) '= (trm_fix f p1 t1 'crash) 'in e)
(at level 200, only parsing) : trm_scope.
Notation "''let_rec_function' f '= ''function' '| p1 '-> t1 '| p2 '-> t2 ''in' e" :=
('let (pat_var f) '= (trm_fix f p1 t1 ('fun p2 '-> t2)) 'in e)
(at level 200) : trm_scope.
Notation "''let_rec_function' f '= ''function' '| p1 '-> t1 '| p2 '-> t2 '| p3 '-> t3 ''in' e" :=
('let (pat_var f) '= (trm_fix f p1 t1 ('function '| p2 '-> t2 '| p3 '-> t3)) 'in e)
(at level 200) : trm_scope.
Notation "''let_rec_function' f '= ''function' '| p1 '-> t1 '| p2 '-> t2 '| p3 '-> t3 '| p4 '-> t4 ''in' e" :=
('let (pat_var f) '= (trm_fix f p1 t1 ('function '| p2 '-> t2 '| p3 '-> t3 '| p4 '-> t4)) 'in e)
(at level 200) : trm_scope.
Notation "''let_rec_function' f '= ''function' '| p1 '-> t1 '| p2 '-> t2 '| p3 '-> t3 '| p4 '-> t4 '| p5 '-> t5 ''in' e" :=
('let (pat_var f) '= (trm_fix f p1 t1 ('function '| p2 '-> t2 '| p3 '-> t3 '| p4 '-> t4 '| p5 '-> t5)) 'in e)
(at level 200) : trm_scope.
Notation "''if' t1 ''then' t2 ''else' t3" :=
('match t1 'with '| pat_con con_true nil '-> t2
'| pat_con con_false nil '-> t3)
(at level 200, right associativity,
format "''if' t1 '/' ''then' t2 '/' ''else' t3").
Notation "'_" :=
(pat_wildcard) (at level 0) : pat_scope.
Notation "p 'as x" := (pat_alias x p)
(at level 60, only parsing) : pat_scope.
Notation "'##' n" := (pat_int n)
(at level 50, format "## n") : pat_scope.
Notation "'##' 'true'" := (pat_con con_true nil)
(at level 50, format "## true") : pat_scope.
Notation "'##' 'false'" := (pat_con con_false nil)
(at level 50, format "## false") : pat_scope.
Notation "'[]" := (pat_con con_nil nil)
(at level 0) : pat_scope.
Notation "'[]" := (trm_con con_nil nil)
(at level 0) : trm_scope.
Notation "'[]" := (val_con con_nil nil)
(at level 0) : val_scope.
Notation "h ':: t" := (pat_con con_cons ((h%pat)::(t%pat)::nil))
(at level 41, right associativity) : pat_scope.
Notation "h ':: t" := (trm_con con_cons ((h%trm)::(t%trm)::nil))
(at level 41, right associativity) : trm_scope.
Notation "h ':: t" := (val_con con_cons ((h%val)::(t%val)::nil))
(at level 41, right associativity) : val_scope.
Notation "h ':: t" := (pat_con con_cons (((h:pat)%pat)::((t:pat)%pat)::nil))
(at level 41, right associativity) : pat_scope.
Notation "h ':: t" := (trm_con con_cons (((h:trm)%trm)::((t:trm)%trm)::nil))
(at level 41, right associativity) : trm_scope.
Notation "h ':: t" := (val_con con_cons (((h:val)%val)::((t:val)%val)::nil))
(at level 41, right associativity) : val_scope.
Notation "''[' x1 ]" := (((x1:trm) ':: '[]))
(at level 50) : trm_scope.
Notation "''[' x1 ; x2 ]" := (((x1:trm) ':: (x2:trm) ':: '[]))
(at level 50) : trm_scope.
Notation "''[' x1 ; x2 ; x3 ]" := (((x1:trm) ':: (x2:trm) ':: (x3:trm) ':: '[]))
(at level 50) : trm_scope.
Notation "''let_rec_fun' f '= ''fun' p1 '-> t" :=
(val_fix f p1 t 'crash)
(at level 200, f at level 0, p1 at level 0) : val_scope.
Notation "''let_rec_fun' f '= ''fun' p1 '-> ''fun' p2 '-> t" :=
(val_fix f p1 ('fun p2 '-> t) 'crash)
(at level 200, f at level 0, p1 at level 0, p2 at level 0) : val_scope.
Notation "''let_rec_fun' f '= ''fun' p1 '-> ''fun' p2 '-> ''fun' p3 '-> t" :=
(val_fix f p1 ('fun p2 p3 '-> t) 'crash)
(at level 200, f at level 0, p1 at level 0, p2 at level 0, p3 at level 0) : val_scope.
Notation "''let_rec_fun' f '= ''fun' p1 '-> ''fun' p2 '-> ''fun' p3 '-> ''fun' p4 '-> t" :=
(val_fix f p1 ('fun p2 p3 p4 '-> t) 'crash)
(at level 200, f at level 0, p1 at level 0, p2 at level 0, p3 at level 0, p4 at level 0) : val_scope.
Notation "''let_rec_function' f '= ''function' '| p1 '-> t1" :=
(val_fix f p1 t1 'crash)
(at level 200, f at level 0, only parsing) : val_scope.
Notation "''let_rec_function' f '= ''function' '| p1 '-> t1 '| p2 '-> t2" :=
(val_fix f p1 t1 ('fun p2 '-> t2))
(at level 200, f at level 0) : val_scope.
Notation "''let_rec_function' f '= ''function' '| p1 '-> t1 '| p2 '-> t2 '| p3 '-> t3" :=
(val_fix f p1 t1 ('function '| p2 '-> t2 '| p3 '-> t3))
(at level 200, f at level 0) : val_scope.
Notation "''let_rec_function' f '= ''function' '| p1 '-> t1 '| p2 '-> t2 '| p3 '-> t3 '| p4 '-> t4" :=
(val_fix f p1 t1 ('function '| p2 '-> t2 '| p3 '-> t3 '| p4 '-> t4))
(at level 200, f at level 0) : val_scope.
Notation "''let_rec_function' f '= ''function' '| p1 '-> t1 '| p2 '-> t2 '| p3 '-> t3 '| p4 '-> t4 '| p5 '-> t5" :=
(val_fix f p1 t1 ('function '| p2 '-> t2 '| p3 '-> t3 '| p4 '-> t4 '| p5 '-> t5))
(at level 200, f at level 0) : val_scope.
Notation "''fun' p1 ''->' t" :=
(val_fix novar p1 t 'crash)
(at level 200, p1 at level 0) : val_scope.
Notation "''fun' p1 p2 '-> t" :=
(('fun p1%pat '-> ('fun p2%pat '-> t)%trm)%val)
(at level 200, p1 at level 0, p2 at level 0) : val_scope.
Notation "''fun' p1 p2 p3 '-> t" :=
(('fun p1%pat '-> ('fun p2%pat p3%pat '-> t)%trm)%val)
(at level 200, p1 at level 0, p2 at level 0,
p3 at level 0) : val_scope.
Notation "''fun' p1 p2 p3 p4 '-> t" :=
(('fun p1%pat '-> ('fun p2%pat p3%pat p4%pat '-> t)%trm)%val)
(at level 200, p1 at level 0, p2 at level 0, p3 at level 0,
p4 at level 0) : val_scope.
Notation "''fun' p1 p2 p3 p4 p5 '-> t" :=
(('fun p1%pat '-> ('fun p2%pat p3%pat p4%pat p5%pat '-> t)%trm)%val)
(at level 200, p1 at level 0, p2 at level 0, p3 at level 0,
p4 at level 0, p5 at level 0) : val_scope.
Notation "''function' '| p1 '-> t1" :=
(('fun p1%pat '-> t1)%val)
(at level 200, only parsing) : val_scope.
Notation "''function' '| p1 '-> t1 '| p2 '-> t2" :=
(val_fix novar p1%pat t1 ('function '| p2%pat '-> t2)%trm)
(at level 200) : val_scope.
Notation "''function' '| p1 '-> t1 '| p2 '-> t2 '| p3 '-> t3" :=
(val_fix novar p1%pat t1 ('function '| p2%pat '-> t2 '| p3%pat '-> t3)%trm)
(at level 200) : val_scope.
Notation "''function' '| p1 '-> t1 '| p2 '-> t2 '| p3 '-> t3 '| p4 '-> t4" :=
(val_fix novar p1%pat t1 ('function '| p2%pat '-> t2 '| p3%pat '-> t3 '| p4%pat '-> t4)%trm)
(at level 200) : val_scope.
Notation "''function' '| p1 '-> t1 '| p2 '-> t2 '| p3 '-> t3 '| p4 '-> t4 '| p5 '-> t5" :=
(val_fix novar p1%pat t1 ('function '| p2%pat '-> t2 '| p3%pat '-> t3 '| p4%pat '-> t4 '| p5%pat '-> t5)%trm)
(at level 200) : val_scope.
Notation "x1 ', x2" := ((#((x1:pat),(x2:pat)))%pat) (at level 42) : pat_scope.
Notation "x1 ', x2" := ((#((x1:trm),(x2:trm)))%trm) (at level 42) : trm_scope.
Notation "x1 ', x2" := ((#((x1:val),(x2:val)))%val) (at level 42) : val_scope.