X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fhelp%2FC%2Fsec_commands.xml;h=102e375adb5658efcfb116293b9b62c0145526c2;hb=d5216e897267e4495290ecbf08eb9f88f6815a0c;hp=4fe77d7b78a8dc3e4871322b5d6a5c736ce11ccb;hpb=5c1b44dfefa085fbb56e23047652d3650be9d855;p=helm.git
diff --git a/helm/software/matita/help/C/sec_commands.xml b/helm/software/matita/help/C/sec_commands.xml
index 4fe77d7b7..102e375ad 100644
--- a/helm/software/matita/help/C/sec_commands.xml
+++ b/helm/software/matita/help/C/sec_commands.xml
@@ -74,26 +74,62 @@
+
+ eval
+ eval red on t
+
+
+
+ Synopsis:
+
+ eval
+ &reduction-kind;
+ on
+ &term;
+
+
+
+ Action:
+
+ Opens a CIC browser window that shows
+ the reduct of
+ t
+ together with its type.
+
+
+
+
+
coercion
- coercion u
+ coercion u with ariety saturation nocomposites
Synopsis:
- coercion &uri;
+
+ coercion
+ (&uri; | &term; with)
+ [ &nat; [&nat;]]
+ [ nocomposites ]
+
Action:
- Declares u as an implicit coercion
- from the type of its last argument (source)
- to its codomain (target). Every time a term x
+ Declares u as an implicit coercion.
+ If the type of u is
+ âx1:T1. ⦠âx(n-1):T(n-1).Tn the coercion target is
+ T(n - ariety) while its source is
+ T(n - ariety - saturation - 1).
+ Every time a term x
of type source is used with expected type target, Matita
automatically replaces x with
- (u ? ⦠? x) to avoid a typing error.
+ (u ? ⦠? x ? ⦠?) to avoid a typing error.
+ Note that the number of ? added after
+ x is saturation.
Implicit coercions are not displayed to the user:
(u ? ⦠? x) is rendered simply
as x.
@@ -102,7 +138,8 @@
and there is already a coercion u' of
target s or source t,
a composite implicit coercion is automatically computed
- by Matita.
+ by Matita unless nocomposites
+ is specified.