Skip to content
Snippets Groups Projects

Make [ELCtx_Alive] a coercion

Merged Jacques-Henri Jourdan requested to merge jh/alive_coercions into master
1 file
+ 15
10
Compare changes
  • Side-by-side
  • Inline
+ 15
10
@@ -98,16 +98,21 @@ End fn.
@@ -98,16 +98,21 @@ End fn.
Arguments fn_params {_ _} _.
Arguments fn_params {_ _} _.
(* TODO: Once we depend on 8.6pl1, extend this to recursive binders so that
(* We use recursive notation for binders as well, to allow patterns
patterns like '(a, b) can be used. *)
like '(a, b) to be used. In practice, only one binder is ever used,
Notation "'fn(∀' x ',' E ';' T1 ',' .. ',' TN ')' '→' R" :=
but using recursive binders is the only way to make Coq accept
(fn (λ x, FP (Vector.cons T1 .. (Vector.cons TN Vector.nil) ..)%T R%T E%EL))
patterns. *)
(at level 99, R at level 200,
(* FIXME : because of a bug in Coq, such patterns only work for
format "'fn(∀' x ',' E ';' T1 ',' .. ',' TN ')' '→' R") : lrust_type_scope.
printing. Once on 8.6pl1, this should work. *)
Notation "'fn(∀' x ',' E ')' '→' R" :=
Notation "'fn(∀' x .. x' ',' E ';' T1 ',' .. ',' TN ')' '→' R" :=
(fn (λ x, FP Vector.nil R%T E%EL))
(fn (λ x, (.. (λ x',
(at level 99, R at level 200,
FP (Vector.cons T1 .. (Vector.cons TN Vector.nil) ..)%T R%T E%EL)..)))
format "'fn(∀' x ',' E ')' '→' R") : lrust_type_scope.
(at level 99, R at level 200, x binder, x' binder,
 
format "'fn(∀' x .. x' ',' E ';' T1 ',' .. ',' TN ')' '→' R") : lrust_type_scope.
 
Notation "'fn(∀' x .. x' ',' E ')' '→' R" :=
 
(fn (λ x, (.. (λ x', FP Vector.nil R%T E%EL)..)))
 
(at level 99, R at level 200, x binder, x' binder,
 
format "'fn(∀' x .. x' ',' E ')' '→' R") : lrust_type_scope.
Notation "'fn(' E ';' T1 ',' .. ',' TN ')' '→' R" :=
Notation "'fn(' E ';' T1 ',' .. ',' TN ')' '→' R" :=
(fn (λ _:(), FP (Vector.cons T1 .. (Vector.cons TN Vector.nil) ..) R%T E%EL) )
(fn (λ _:(), FP (Vector.cons T1 .. (Vector.cons TN Vector.nil) ..) R%T E%EL) )
(at level 99, R at level 200,
(at level 99, R at level 200,
Loading