Skip to content

\vassign allows an expression as the second argument #16

@kohlhase

Description

@kohlhase

Currently \vassign is treated like \tassign, and that is incorrect. In \tassign{a}{b}, both a and b are symbol names; from the source and the target theory.
In \vassign{a}{e} is a mathematical object (from the target theory), so e should not be checked (it can essentially be anything), or at least be checked as $e$ would be.

This is also one of the top-error-producing bugs.

Metadata

Metadata

Assignees

Labels

bugSomething isn't workingpriorityShould be handled with priority

Type

No type

Projects

No projects

Milestone

No milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions