Skip to content

allow (but ignore) unary $distinct#832

Merged
MichaelRawson merged 1 commit intomasterfrom
michael-unary-distinct
Mar 26, 2026
Merged

allow (but ignore) unary $distinct#832
MichaelRawson merged 1 commit intomasterfrom
michael-unary-distinct

Conversation

@MichaelRawson
Copy link
Copy Markdown
Contributor

Fixes #828.

@MichaelRawson MichaelRawson force-pushed the michael-unary-distinct branch from f8fb384 to c71e865 Compare March 25, 2026 15:30
@MichaelRawson MichaelRawson merged commit 52167ec into master Mar 26, 2026
1 check passed
@MichaelRawson MichaelRawson deleted the michael-unary-distinct branch March 26, 2026 10:14
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

TPTP keyword $distinct should also accept 1 term.

2 participants