Verified Commit 35646ff0 authored by Julien's avatar Julien
Browse files

WIP custom labels

parent 38705cac
Pipeline #131412047 failed with stage
in 8 minutes and 2 seconds
......@@ -331,6 +331,8 @@ Proof.
try (apply IHs1; auto).
Qed.
Definition custom_label := (string * nat)%type.
(* Module Type TType. *)
(* Parameter T : Type. *)
(* End TType. *)
......
......@@ -8,9 +8,17 @@ grammar
%% Types
user_label :: 'user_label_' ::= {{coq string}} {{com Label / variable}}
| id :: S :: id {{coq [[id]]}} {{ocaml (Aux.explode [[id]])}}
custom_label :: 'custom_label_' ::= {{coq custom_label}}
| id :: S :: id {{coq [[id]]}} {{ocaml (Aux.explode [[id]])}}
% We do not distinguish variables from field labels (nor environments from records)
label, l, var, x :: 'label_' ::= {{coq string}} {{com Label / variable}}
| id :: S :: user {{coq [[id]]}} {{ocaml (Aux.explode [[id]])}}
label, l, var, x :: 'label_' ::= {{coq string}} {{com Label / variable}}
| user_label :: :: user
| custom_label :: :: custom
rty :: 'rty_' ::= {{com Record type}}
| { l_1 : ty_1 ; .. ; l_n : ty_n } :: :: record
......@@ -120,7 +128,7 @@ defns
% G |- { l_1 : ty_1 ; .. ; l_n : ty_n } @ { l'_1 : ty'_1 ; .. ; l'_m : ty'_m } == { l_1 : ty_1 ; .. ; l_n : ty_n ; l'_1 : ty'_1 ; .. ; l'_m : ty'_m }
% defn
% G |- | ty | :: :: type_canon :: Tcanon_ {{com Canonicity of type}} by
% G |- | ty | :: :: type_canon :: Tcanon_ {{com Canonicity of type}} by
% G |- | ty_1 | .. G |- | ty_n |
% sorted { l_1 ; .. ; l_n }
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment