| BYC_letsuchthat of string * CicNotationPt.term * string * CicNotationPt.term
| BYC_wehaveand of string * CicNotationPt.term * string * CicNotationPt.term
+let out = ref ignore
+
+let set_callback f = out := f
+
EXTEND
GLOBAL: term statement;
constructor: [ [ name = IDENT; SYMBOL ":"; typ = term -> (name, typ) ] ];
GrafiteAst.Obj (loc, Ast.Theorem (`Axiom, name, typ, None))
| "let"; ind_kind = [ "corec" -> `CoInductive | "rec"-> `Inductive ];
defs = CicNotationParser.let_defs ->
+ (* In case of mutual definitions here we produce just
+ the syntax tree for the first one. The others will be
+ generated from the completely specified term just before
+ insertion in the environment. We use the flavour
+ `MutualDefinition to rememer this. *)
let name,ty =
match defs with
| (params,(Ast.Ident (name, None), Some ty),_,_) :: _ ->
| _ -> assert false
in
let body = Ast.Ident (name,None) in
- GrafiteAst.Obj (loc, Ast.Theorem(`Definition, name, ty,
- Some (Ast.LetRec (ind_kind, defs, body))))
+ let flavour =
+ if List.length defs = 1 then
+ `Definition
+ else
+ `MutualDefinition
+ in
+ GrafiteAst.Obj (loc, Ast.Theorem(flavour, name, ty,
+ Some (Ast.LetRec (ind_kind, defs, body))))
| IDENT "inductive"; spec = inductive_spec ->
let (params, ind_types) = spec in
GrafiteAst.Obj (loc, Ast.Inductive (params, ind_types))
(loc,GrafiteAst.Include (iloc,buri))))
| scom = lexicon_command ; SYMBOL "." ->
fun ~include_paths status ->
- let status = LexiconEngine.eval_command status scom in
+ !out scom;
+ let status = LexiconEngine.eval_command status scom in
status,LNone loc
| EOI -> raise End_of_file
]