Permalink
Browse files

Documentation for raw_match_type was out of date.

  • Loading branch information...
1 parent 0da0f0c commit 257d4ee3cb3d1b0fa82976519ceae873ffdbedfb @acjf3 acjf3 committed Dec 8, 2012
Showing with 12 additions and 13 deletions.
  1. +12 −13 help/Docfiles/Type.raw_match_type.doc
@@ -1,11 +1,10 @@
\DOC raw_match_type
\BLTYPE
-raw_match_type
- : hol_type list
- -> hol_type -> hol_type
- -> (hol_type,hol_type) subst * hol_type list
- -> (hol_type,hol_type) subst * hol_type list
+raw_match_type
+ : hol_type -> hol_type ->
+ (hol_type,hol_type) subst * hol_type list ->
+ (hol_type,hol_type) subst * hol_type list
\ELTYPE
\SYNOPSIS
@@ -15,26 +14,26 @@ Primitive type matching algorithm.
type, matching.
\DESCRIBE
-An invocation {raw_match_type away pat ty (S,Id)} performs matching, just
-as {match_tyl}, except that it takes an extra accumulating parameter
+An invocation {raw_match_type pat ty (S,Id)} performs matching, just
+as {match_type}, except that it takes an extra accumulating parameter
{(S,Id)}, which represents a 'raw' substitution that the match
{(theta,id)} of {pat} and {ty} must be compatible with. If matching is
successful, {(theta,id)} is merged with {(S,Id)} to yield the result.
\FAILURE
-A call to {raw_match_type away pat ty (S,Id)} will fail
-when {match_typel away pat ty} would. It will also fail when a
+A call to {raw_match_type pat ty (S,Id)} will fail
+when {match_type pat ty} would. It will also fail when a
{{redex,residue}} calculated in the course of matching {pat} and {ty}
is such that there is a {{redex_i,residue_i}} in {S} and {redex}
equals {redex_i} but {residue} does not equal {residue_i}.
\EXAMPLE
{
-- val res1 = raw_match_type [] alpha (alpha --> bool) ([],[]);
+- val res1 = raw_match_type alpha (alpha --> bool) ([],[]);
> val it = ([{redex = `:'a`, residue = `:'a -> bool`}], []) : ...
-- raw_match_type [] (alpha --> beta --> gamma)
- ((alpha --> bool) --> beta --> ind) res1;
+- raw_match_type (alpha --> beta --> gamma)
+ ((alpha --> bool) --> beta --> ind) res1;
> val it =([{redex = `:'c`, residue = `:ind`},
{redex = `:'a`, residue = `:'a -> bool`}], [`:'b`]) : ....
}
@@ -44,5 +43,5 @@ equals {redex_i} but {residue} does not equal {residue_i}.
Probably exposes too much internal state of the matching algorithm.
\SEEALSO
-Type.match_type, Type.match_typel.
+Type.match_type
\ENDDOC

0 comments on commit 257d4ee

Please sign in to comment.