Ho node manager types (#1203)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 11 Oct 2017 02:07:14 +0000 (21:07 -0500)
committerGitHub <noreply@github.com>
Wed, 11 Oct 2017 02:07:14 +0000 (21:07 -0500)
commit5e2c7c3a25d334c0068b423225f8ff7793260069
tree1ba631e008f7c482f8d0fdcac87b23090e6a2920
parentdd979fcdb5a952462e4d6702999b5354de5a7be8
Ho node manager types (#1203)

* Remove restrictions about function types

* Introduce notion of first-class type, improve assertions, add comment on equality type rule.

* Update comment
src/expr/node_manager.h
src/expr/type.h
src/expr/type_node.cpp
src/expr/type_node.h
src/theory/builtin/theory_builtin_type_rules.h