summaryrefslogtreecommitdiff
path: root/src/theory/uf/kinds
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/uf/kinds')
-rw-r--r--src/theory/uf/kinds3
1 files changed, 3 insertions, 0 deletions
diff --git a/src/theory/uf/kinds b/src/theory/uf/kinds
index e2d740e20..500295a0c 100644
--- a/src/theory/uf/kinds
+++ b/src/theory/uf/kinds
@@ -29,4 +29,7 @@ typerule PARTIAL_APPLY_UF ::CVC4::theory::uf::PartialTypeRule
operator CARDINALITY_VALUE 1 "cardinality value of sort S: first parameter is (any) term of sort S"
typerule CARDINALITY_VALUE ::CVC4::theory::uf::CardinalityValueTypeRule
+operator HO_APPLY 2 "higher-order (partial) function application"
+typerule HO_APPLY ::CVC4::theory::uf::HoApplyTypeRule
+
endtheory
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback