From f94eb70000832bc252cd4a510a1ede4d8197a4a8 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 4 Jul 2005 14:09:02 +0000 Subject: [PATCH] New command default "foo" uri1 ... urin to set uri1 ... urin as the default foo. Actually it can be used to set the current equality, true, false and absurd like this: default "equality" equri sym_equri transeq_uri eq_induri eq_ind_ruri. default "true" trueuri. default "false" falseuri. default "absurd" absurduri. --- helm/matita/library/equality.ma | 7 +++++++ helm/matita/library/logic.ma | 6 ++++++ helm/matita/matitaEngine.ml | 9 +++++++-- 3 files changed, 20 insertions(+), 2 deletions(-) diff --git a/helm/matita/library/equality.ma b/helm/matita/library/equality.ma index d700ddd07..90ce050e3 100644 --- a/helm/matita/library/equality.ma +++ b/helm/matita/library/equality.ma @@ -38,6 +38,13 @@ theorem f_equal: \forall A,B:Type.\forall f:A\to B. intros.elim H.reflexivity. qed. +default "equality" + cic:/matita/equality/eq.ind + cic:/matita/equality/sym_eq.con + cic:/matita/equality/trans_eq.con + cic:/matita/equality/eq_ind.con + cic:/matita/equality/eq_ind_r.con. + theorem f_equal2: \forall A,B,C:Type.\forall f:A\to B \to C. \forall x1,x2:A. \forall y1,y2:B. eq A x1 x2\to eq B y1 y2\to eq C (f x1 y1) (f x2 y2). diff --git a/helm/matita/library/logic.ma b/helm/matita/library/logic.ma index a509bbb8d..fd3744396 100644 --- a/helm/matita/library/logic.ma +++ b/helm/matita/library/logic.ma @@ -18,8 +18,12 @@ set "baseuri" "cic:/matita/logic/". inductive True: Prop \def I : True. +default "true" cic:/matita/logic/True.ind. + inductive False: Prop \def . +default "false" cic:/matita/logic/False.ind. + definition Not: Prop \to Prop \def \lambda A. (A \to False). @@ -27,6 +31,8 @@ theorem absurd : \forall A,C:Prop. A \to Not A \to C. intros. elim (H1 H). qed. +default "absurd" cic:/matita/logic/absurd.ind. + inductive And (A,B:Prop) : Prop \def conj : A \to B \to (And A B). diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml index df8f484ba..cb420d267 100644 --- a/helm/matita/matitaEngine.ml +++ b/helm/matita/matitaEngine.ml @@ -224,6 +224,10 @@ let eval_from_stream_ref = ref (fun _ _ _ -> assert false);; let eval_command status cmd = match cmd with + | TacticAst.Default (loc, what, uris) as cmd -> + LibraryObjects.set_default what uris; + {status with moo_content_rev = + (TacticAstPp.pp_command cmd ^ "\n") :: status.moo_content_rev} | TacticAst.Include (loc, path) -> let path = MatitaMisc.obj_file_of_script path in let stream = Stream.of_channel (open_in path) in @@ -536,13 +540,14 @@ and disambiguate_tacticals status tacticals = status, tacticals let disambiguate_command status = function - | TacticAst.Include (loc,path) as cmd -> status,cmd + | TacticAst.Default _ + | TacticAst.Alias _ + | TacticAst.Include _ as cmd -> status,cmd | TacticAst.Coercion (loc, term) -> let status, term = disambiguate_term status term in status, TacticAst.Coercion (loc,term) | (TacticAst.Set _ | TacticAst.Qed _ | TacticAst.Drop _ ) as cmd -> status, cmd - | TacticAst.Alias _ as x -> status, x | TacticAst.Obj (loc,obj) -> let status,obj = disambiguate_obj status obj in status, TacticAst.Obj (loc,obj) -- 2.39.2