Commit df9875a9 authored by MARCHE Claude's avatar MARCHE Claude

improved documentation of transf compute

parent 3608ecd5
......@@ -274,6 +274,18 @@ meta "rewrite" prop a
from left to right. Beware that there is no check for termination
nor for confluence of the set of rewrite rules declared.
\end{itemize}
Instead of using a meta, it is possible to declare an axiom as a
rewrite rule by adding the label \verb|"rewrite"| on the axiom name or
on the axiom itself, e.g.:
\begin{whycode}
axiom a "rewrite": forall ... t1 = t2
lemma b: "rewrite" forall ... f1 <-> f2
\end{whycode}
The second form allows some form of local rewriting, e.g.
\begin{whycode}
lemma l: forall x y. ("rewrite" x = y) -> f x = f y
\end{whycode}
can be proved by \verb|introduce_premises| followed by \verb|"compute_specified"|.
\paragraph{Bound on the number of reductions}
The computations performed by these transformations can take an
......
......@@ -40,7 +40,10 @@ let rule_label = Ident.create_label "rewrite"
let collect_rule_decl prs e d =
match d.Decl.d_node with
| Decl.Dprop((Plemma|Paxiom), pr, t) ->
if Decl.Spr.mem pr prs || Ident.Slab.mem rule_label t.t_label then
if Decl.Spr.mem pr prs ||
Ident.Slab.mem rule_label pr.pr_name.Ident.id_label ||
Ident.Slab.mem rule_label t.t_label
then
try add_rule t e
with NotARewriteRule msg ->
Warning.emit "proposition %a cannot be turned into a rewrite rule: %s"
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment