Keyboard shortcuts

Press or to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

mk_res_abstract

res_quanLib.mk_res_abstract : (term # term # term) -> term

Term constructor for restricted abstraction.

mk_res_abstract("var","P","t") returns "\var :: P . t".

Failure

Fails with mk_res_abstract if the first term is not a variable or if P and t are not of type ":bool".

See also

res_quanLib.dest_res_abstract, res_quanLib.is_res_abstract