BeHOLd.ClassicalHOL.Patterns (behold v1.1.3)
View SourceDefines patterns on terms with respect to the definitions introduced in
BeHOLd.ClassicalHOL.Definitions. Note that this should only be used for
pattern matching and not for term construction!
Summary
Functions
Pattern to match the conjunction of two terms.
Pattern to match the disjunction of two terms.
Pattern to match equiality of two terms, ignoring the type.
Pattern to match the equivalence of two terms.
Pattern to match the existential quantification of a given predicate, ignoring the type.
Pattern to match the implication of two terms, where the first term implies the second.
Pattern to match a negated term.
Pattern to match equality of two terms with respect to their type.
Pattern to match the existential quantification of a given predicate with respect to its type.
Pattern to match the universal quantification of a given predicate with respect to its type.
Pattern to match the universal quantification of a given predicate ignoring the type.
Functions
@spec conjunction(HOL.Data.hol_term(), HOL.Data.hol_term()) :: HOL.Data.hol_term()
Pattern to match the conjunction of two terms.
@spec disjunction(HOL.Data.hol_term(), HOL.Data.hol_term()) :: HOL.Data.hol_term()
Pattern to match the disjunction of two terms.
@spec equality(HOL.Data.hol_term(), HOL.Data.hol_term()) :: HOL.Data.hol_term()
Pattern to match equiality of two terms, ignoring the type.
@spec equivalence(HOL.Data.hol_term(), HOL.Data.hol_term()) :: HOL.Data.hol_term()
Pattern to match the equivalence of two terms.
@spec existential_quantification(HOL.Data.hol_term()) :: HOL.Data.hol_term()
Pattern to match the existential quantification of a given predicate, ignoring the type.
@spec implication(HOL.Data.hol_term(), HOL.Data.hol_term()) :: HOL.Data.hol_term()
Pattern to match the implication of two terms, where the first term implies the second.
@spec negated(HOL.Data.hol_term()) :: HOL.Data.hol_term()
Pattern to match a negated term.
@spec typed_equality(HOL.Data.hol_term(), HOL.Data.hol_term(), HOL.Data.type()) :: HOL.Data.hol_term()
Pattern to match equality of two terms with respect to their type.
@spec typed_existential_quantification(HOL.Data.hol_term(), HOL.Data.type()) :: HOL.Data.hol_term()
Pattern to match the existential quantification of a given predicate with respect to its type.
@spec typed_universal_quantification(HOL.Data.hol_term(), HOL.Data.type()) :: HOL.Data.hol_term()
Pattern to match the universal quantification of a given predicate with respect to its type.
@spec universal_quantification(HOL.Data.hol_term()) :: HOL.Data.hol_term()
Pattern to match the universal quantification of a given predicate ignoring the type.