(head, vars)
]
];
+ arg: [
+ [ PAREN "(" ; names = LIST1 IDENT SEP SYMBOL ",";
+ SYMBOL ":"; ty = term; PAREN ")" -> names,ty
+ | name = IDENT -> [name],CicAst.Implicit
+ ]
+ ];
let_defs:[
[ defs = LIST1 [
name = IDENT;
- args = LIST1 [
- PAREN "(" ; names = LIST1 IDENT SEP SYMBOL ",";
- SYMBOL ":"; ty = term; PAREN ")" ->
- (names, Some ty)
- | name = IDENT -> [name],None
- ];
+ args = LIST1 [arg = arg -> arg];
index_name = OPT [ IDENT "on"; idx = IDENT -> idx ];
ty = OPT [ SYMBOL ":" ; t = term -> t ];
SYMBOL <:unicode<def>> (* ≝ *);
list_of_binder binder ty
(binder_of_arg_list binder final_term tl) l
in
- let args =
- List.map
- (function
- names,Some ty -> names,ty
- | names,None -> names,CicAst.Implicit
- ) args in
let t1' = binder_of_arg_list `Lambda t1 args in
let ty' =
match ty with
]
];
inductive_spec: [ [
- fst_name = IDENT; params = LIST0 [
- PAREN "("; names = LIST1 IDENT SEP SYMBOL ","; SYMBOL ":";
- typ = term; PAREN ")" -> (names, typ) ];
+ fst_name = IDENT; params = LIST0 [ arg=arg -> arg ];
SYMBOL ":"; fst_typ = term; SYMBOL <:unicode<def>>; OPT SYMBOL "|";
fst_constructors = LIST0 constructor SEP SYMBOL "|";
tl = OPT [ "with";
let ind_types = fst_ind_type :: tl_ind_types in
(params, ind_types)
] ];
-
+
+ record_spec: [ [
+ name = IDENT; params = LIST0 [ arg = arg -> arg ] ;
+ SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>; PAREN "{" ;
+ fields = LIST0 [
+ name = IDENT ; SYMBOL ":" ; ty = term -> (name,ty)
+ ] SEP SYMBOL ";"; PAREN "}" ->
+ let params =
+ List.fold_right
+ (fun (names, typ) acc ->
+ (List.map (fun name -> (name, typ)) names) @ acc)
+ params []
+ in
+ (params,name,typ,fields)
+ ] ];
+
macro: [
[ [ IDENT "quit" ] -> TacticAst.Quit loc
(* | [ IDENT "abort" ] -> TacticAst.Abort loc *)
| flavour = theorem_flavour; name = OPT IDENT; SYMBOL ":"; typ = term;
body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
TacticAst.Theorem (loc, flavour, name, typ, body)
+ | flavour = theorem_flavour; name = OPT IDENT;
+ body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
+ TacticAst.Theorem (loc, flavour, name, CicAst.Implicit, body)
| "let"; ind_kind = [ "corec" -> `CoInductive | "rec"-> `Inductive ];
defs = let_defs ->
let name,ty =
TacticAst.Coercion (loc, CicAst.Uri (name,Some []))
| [ IDENT "alias" ]; spec = alias_spec ->
TacticAst.Alias (loc, spec)
+ | [ IDENT "record" ]; (params,name,ty,fields) = record_spec ->
+ TacticAst.Record (loc, params,name,ty,fields)
]];
executable: [