search

david-a-wheeler / mmverify.py

Metamath verifier in Python
MIT License
35 stars 10 forks source link

I am not sure what `dvs` supposed to be. #2

Closed treeform closed 2 years ago

treeform commented 2 years ago

I am not sure what dvs supposed to be. It always appear to be {} for current set.mm ( https://github.com/metamath/set.mm/blob/develop/set.mm )?

https://github.com/david-a-wheeler/mmverify.py/blob/master/mmverify.py#L157

treeform commented 2 years ago

Sorry I was wrong, its needed for the "disjoint violation" error, my mistake.