diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-04-09 11:18:18 -0400 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-04-09 17:46:21 -0400 |
| commit | ec4d1e3753434f5d34a22e653dace14b87557aaf (patch) | |
| tree | 9cfa4fc484dd5e27373277751887e50558a458df /src/theory/builtin | |
| parent | e93d0be650b9f349fe8be3a56ce2fc7cb20fddf0 (diff) | |
Minor change to better support parameterized partial/total kinds (for upcoming datatypes work).
Diffstat (limited to 'src/theory/builtin')
| -rw-r--r-- | src/theory/builtin/kinds | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds index b51feea6d..b3383e6c4 100644 --- a/src/theory/builtin/kinds +++ b/src/theory/builtin/kinds @@ -97,9 +97,9 @@ # # operator PLUS 2: "addition on two or more arguments" # -# parameterized K #children ["comment"] +# parameterized K1 K2 #children ["comment"] # -# Declares a "built-in" parameterized operator kind K. This is a +# Declares a "built-in" parameterized operator kind K1. This is a # theory-specific APPLY, e.g., APPLY_UF, which applies its first # parameter (say, "f"), to its operands (say, "x" and "y", making # the full application "f(x,y)"). Nodes with such a kind will @@ -107,7 +107,10 @@ # Node::getOperator() returns the Node of functional type # representing "f" here), and the "children" are defined to be # this operator's parameters, and don't include the operator -# itself (here, there are only two children "x" and "y"). +# itself (here, there are only two children "x" and "y"). The +# operator ("f") should have kind K2 (and this should be enforced +# by the custom typechecker, at present this isn't done uniformly +# by the expression package). # # LB and UB are the same as documented for the operator command, # except that parameterized operators may have zero children. The |