From 5d772cbfa20abfb84b9925a5670ac5dd28312251 Mon Sep 17 00:00:00 2001 From: aarne Date: Thu, 16 Mar 2006 21:26:22 +0000 Subject: MatchTerm: testing conditions on terms, e.g. nodup --- src/HelpFile | 14 ++++++++------ 1 file changed, 8 insertions(+), 6 deletions(-) (limited to 'src/HelpFile') diff --git a/src/HelpFile b/src/HelpFile index 58c4c1262..38b4fdcb2 100644 --- a/src/HelpFile +++ b/src/HelpFile @@ -626,12 +626,14 @@ q, quit: q -startcat, like -cat, but used in grammars (to avoid clash with keyword cat) -transform, transformation performed on a syntax tree. The default is identity. - -transform=identity no change - -transform=compute compute by using definitions in the grammar - -transform=typecheck return the term only if it is type-correct - -transform=solve solve metavariables as derived refinements - -transform=context solve metavariables by unique refinements as variables - -transform=delete replace the term by metavariable + -transform=identity no change + -transform=compute compute by using definitions in the grammar + -transform=nodup return the term only if it has no constants duplicated + -transform=nodupatom return the term only if it has no atomic constants duplicated + -transform=typecheck return the term only if it is type-correct + -transform=solve solve metavariables as derived refinements + -transform=context solve metavariables by unique refinements as variables + -transform=delete replace the term by metavariable -unlexer, untokenization transforming linearization output into a string. The default is unwords. -- cgit v1.2.3