option query_remove_redundancy

Default: true

Sets whether redundant joins (i.e., containing a binding v and an equation v = e where v notin e) should be eliminated. Note that this only has an effect when specified at the top level of a query, not within each block.

Keyword:

eval
simple
unit_query
pi
query_literal
pi
toCoQuery
query_compose
eval
back
fromCoSpan
toQuery
counit_query

Appears in:

All_Syntax