Hets - the Heterogeneous Tool Set

Copyright(c) Christian Maeder Uni Bremen 2005
LicenseGPLv2 or higher, see LICENSE.txt
MaintainerChristian.Maeder@dfki.de
Stabilityprovisional
Portabilityportable
Safe HaskellSafe

CASL.Inject

Description

Replace Sorted_term(s) with explicit injection functions. Don't do this after simplification since crucial sort information may be missing

Synopsis

Documentation

injRecord :: TermExtension f => (f -> f) -> Record f (FORMULA f) (TERM f) Source #

injTerm :: TermExtension f => (f -> f) -> TERM f -> TERM f Source #

injFormula :: TermExtension f => (f -> f) -> FORMULA f -> FORMULA f Source #

insertInjOps :: Sign f e -> [OP_SYMB] -> Sign f e Source #

takes a list of OP_SYMB generated by recover_Sort_gen_ax and inserts these operations into the signature; unqualified OP_SYMBs yield an error