+ grafite_ncommand: [ [
+ IDENT "nqed" -> G.NQed loc
+ | nflavour = ntheorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
+ body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
+ G.NObj (loc, N.Theorem (nflavour, name, typ, body))
+ | nflavour = ntheorem_flavour; name = IDENT; SYMBOL <:unicode<def>> (* ≝ *);
+ body = term ->
+ G.NObj (loc, N.Theorem (nflavour, name, N.Implicit `JustOne, Some body))
+ | IDENT "naxiom"; name = IDENT; SYMBOL ":"; typ = term ->
+ G.NObj (loc, N.Theorem (`Axiom, name, typ, None))
+ | NLETCOREC ; defs = let_defs ->
+ nmk_rec_corec `CoInductive defs loc
+ | NLETREC ; defs = let_defs ->
+ nmk_rec_corec `Inductive defs loc
+ | IDENT "ninductive"; spec = inductive_spec ->
+ let (params, ind_types) = spec in
+ G.NObj (loc, N.Inductive (params, ind_types))
+ | IDENT "ncoinductive"; spec = inductive_spec ->
+ let (params, ind_types) = spec in
+ let ind_types = (* set inductive flags to false (coinductive) *)
+ List.map (fun (name, _, term, ctors) -> (name, false, term, ctors))
+ ind_types
+ in
+ G.NObj (loc, N.Inductive (params, ind_types))
+ | IDENT "universe"; IDENT "constraint"; u1 = tactic_term;
+ strict = [ SYMBOL <:unicode<lt>> -> true
+ | SYMBOL <:unicode<leq>> -> false ];
+ u2 = tactic_term ->
+ let u1 =
+ match u1 with
+ | CicNotationPt.AttributedTerm (_, CicNotationPt.Sort (`NType i)) ->
+ NUri.uri_of_string ("cic:/matita/pts/Type"^i^".univ")
+ | CicNotationPt.AttributedTerm (_, CicNotationPt.Sort (`NCProp i)) ->
+ NUri.uri_of_string ("cic:/matita/pts/CProp"^i^".univ")
+ | _ -> raise (Failure "only a sort can be constrained")
+ in
+ let u2 =
+ match u2 with
+ | CicNotationPt.AttributedTerm (_, CicNotationPt.Sort (`NType i)) ->
+ NUri.uri_of_string ("cic:/matita/pts/Type"^i^".univ")
+ | CicNotationPt.AttributedTerm (_, CicNotationPt.Sort (`NCProp i)) ->
+ NUri.uri_of_string ("cic:/matita/pts/CProp"^i^".univ")
+ | _ -> raise (Failure "only a sort can be constrained")
+ in
+ G.NUnivConstraint (loc, strict,u1,u2)
+ | IDENT "unification"; IDENT "hint"; n = int; t = tactic_term ->
+ G.UnificationHint (loc, t, n)
+ | IDENT "ncoercion"; name = IDENT; SYMBOL ":"; ty = term;
+ SYMBOL <:unicode<def>>; t = term; "on";
+ id = [ IDENT | PIDENT ]; SYMBOL ":"; source = term;
+ "to"; target = term ->
+ G.NCoercion(loc,name,t,ty,(id,source),target)
+ | IDENT "nrecord" ; (params,name,ty,fields) = record_spec ->
+ G.NObj (loc, N.Record (params,name,ty,fields))
+ | IDENT "ncopy" ; s = IDENT; IDENT "from"; u = URI; "with";
+ m = LIST0 [ u1 = URI; SYMBOL <:unicode<mapsto>>; u2 = URI -> u1,u2 ] ->
+ G.NCopy (loc,s,NUri.uri_of_string u,
+ List.map (fun a,b -> NUri.uri_of_string a, NUri.uri_of_string b) m)
+ ]];
+