Skip to content

FreePreorder should not use ObExpr and HomExpr #979

@kris-brown

Description

@kris-brown

As Nate Osgood as shown over Zulip, making the symbolic model use a HomExpr comes with the assumption that the theory has dom and codom available (this gets used in the show method for the hom generators). This assumption is not valid for ThPreorder which has lhs and rhs as its accessors, so there is an error when trying to show them.

A possible solution is to just make the symbolic model use GATExprs.

Metadata

Metadata

Assignees

Labels

Type

No type

Projects

No projects

Milestone

No milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions