From: Ferruccio Guidi Date: Tue, 20 Jun 2006 17:59:04 +0000 (+0000) Subject: - fwd concrete syntax fixed X-Git-Tag: 0.4.95@7852~1286 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a094832a413d3d11cd4031b01a5119452384a7ac;p=helm.git - fwd concrete syntax fixed - decompose, fwd, lapply documentation fixed --- diff --git a/components/grafite/grafiteAstPp.ml b/components/grafite/grafiteAstPp.ml index 9e1dffdcd..20d57ef9e 100644 --- a/components/grafite/grafiteAstPp.ml +++ b/components/grafite/grafiteAstPp.ml @@ -110,7 +110,7 @@ let rec pp_tactic ~term_pp ~lazy_term_pp = (lazy_term_pp term) (pp_tactic_pattern pattern) | FwdSimpl (_, hyp, idents) -> sprintf "fwd %s%s" hyp - (match idents with [] -> "" | idents -> " " ^ pp_idents idents) + (match idents with [] -> "" | idents -> " as " ^ pp_idents idents) | Generalize (_, pattern, ident) -> sprintf "generalize %s%s" (pp_tactic_pattern pattern) (match ident with None -> "" | Some id -> " as " ^ id) diff --git a/components/grafite_parser/grafiteParser.ml b/components/grafite_parser/grafiteParser.ml index 535e396a9..ad081d664 100644 --- a/components/grafite_parser/grafiteParser.ml +++ b/components/grafite_parser/grafiteParser.ml @@ -178,7 +178,7 @@ EXTEND GrafiteAst.Fold (loc, kind, t, p) | IDENT "fourier" -> GrafiteAst.Fourier loc - | IDENT "fwd"; hyp = IDENT; idents = OPT ident_list0 -> + | IDENT "fwd"; hyp = IDENT; idents = OPT [ "as"; idents = LIST1 IDENT -> idents ] -> let idents = match idents with None -> [] | Some idents -> idents in GrafiteAst.FwdSimpl (loc, hyp, idents) | IDENT "generalize"; p=pattern_spec; id = OPT ["as" ; id = IDENT -> id] -> diff --git a/matita/help/C/sec_tactics.xml b/matita/help/C/sec_tactics.xml index c10d2bd33..bc5095fae 100644 --- a/matita/help/C/sec_tactics.xml +++ b/matita/help/C/sec_tactics.xml @@ -389,7 +389,11 @@ Synopsis: - decompose &id; [&id;]… &intros-spec; + + decompose + [([&id;]…)] + &id; &intros-spec; + @@ -750,13 +754,13 @@ its constructor takes no arguments. fwd fwd - fwd H + fwd H as H0 ... Hn Synopsis: - fwd &id; [([&id;]…)] + fwd &id; [as &id; [&id;]…] @@ -775,16 +779,23 @@ its constructor takes no arguments. This tactic is under development. It simplifies the current context by removing H using the following methods: - forward application of a suitable simplification theorem (chosen - automatically) of which the type of H is a - premise, decomposition, rewriting. + forward application (by lapply) of a suitable + simplification theorem, chosen automatically, of which the type + of H is a premise, + decomposition (by decompose), + rewriting (by rewrite). + H0 ... Hn + are passed to the tactics fwd invokes, as + names for the premise they introduce. New sequents to prove: - None. + + The ones opened by the tactics fwd invokes. + @@ -1043,19 +1054,39 @@ its constructor takes no arguments. Pre-conditions: - TODO. + + t must have at least d + independent premises and n must not be + greater than d. + Action: - TODO. + + It invokes letin H ≝ (t ? ... ?) + with enough ?'s to reach the + d-th independent premise of + t + (d is maximum if unspecified). + Then it istantiates (by apply) with + t1, ..., tn + the ?'s corresponding to the first + n independent premises of + t. + Usually the other ?'s preceding the + n-th independent premise of + t are istantiated as a consequence. + New sequents to prove: - TODO. + + The ones opened by the tactics lapply invokes. + diff --git a/matita/help/C/tactic_quickref.xml b/matita/help/C/tactic_quickref.xml index e1f7eb434..6a735eee2 100644 --- a/matita/help/C/tactic_quickref.xml +++ b/matita/help/C/tactic_quickref.xml @@ -38,7 +38,11 @@ cut sterm [as id] - decompose id [id]… intros-spec + + decompose + [([id]…)] + id intros-spec + demodulation pattern @@ -80,7 +84,7 @@ - fwd id [([id]…)] + fwd id [as id [id]…] generalize pattern [as id]