Skip to content

Allow adding only constant (no schematic) symbols to a running theory

Viktor Kuncak requested to merge github/fork/cache-nez/mark-concrete into main

Created by: cache-nez

Highlight the separation between Function/Predicate labels and possible symbols by marking constant function and predicate labels with TheorySymbol.

Merge request reports