Skip to content

fix: pushed proxies are terms (TM)#830

Merged
quickbeam123 merged 1 commit intomasterfrom
martin-fix-hol-parsing
Mar 24, 2026
Merged

fix: pushed proxies are terms (TM)#830
quickbeam123 merged 1 commit intomasterfrom
martin-fix-hol-parsing

Conversation

@quickbeam123
Copy link
Copy Markdown
Collaborator

@quickbeam123 quickbeam123 commented Mar 23, 2026

This fixes a parsing crash for a simple

thf(sy_v_I, type,
    i : $o > $o).

% Conjectures (2)
thf(conj_0, hypothesis,
   ((i = (^[X : $o]: X)))).
thf(conj_1, conjecture,
    (((~) = (^[X : $o]: (~ ((i @ X))))))).

Reason: the (~)-bit is parsed specially not as a negation, but already as the vNOT proxy. Therefore, it must be treated as a bool term and not formula.

@quickbeam123 quickbeam123 requested a review from mezpusz March 23, 2026 15:13
@quickbeam123 quickbeam123 merged commit c0174f8 into master Mar 24, 2026
1 check passed
@quickbeam123 quickbeam123 deleted the martin-fix-hol-parsing branch March 24, 2026 09:45
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.

2 participants