|
|
|---|
|
|
|
|---|
b* binder for checking and propagating error results of the fixtype reserr.
This is somewhat similar to ACL2::patbind-er, but it is for result types.
It checks whether the value of the bound term is an error, returning the same error if the check succeeds. Otherwise, the binder proceeds with the rest of the computation.
This binder is used as follows:
(b* (... ((ok <pattern>) <term>) ...) ...)
Note that the argument of
In order to support such a pattern, we generate an initial binding to a variable, a test of whether it is an error or not, and then a second binding of the pattern to the variable if not. As done in other binders that come with b*, we pick a name for the first variable that is unlikely to occur in code.