search

tlaplus / tlapm

The TLA Proof Manager
https://proofs.tlapl.us/
BSD 2-Clause "Simplified" License
65 stars 20 forks source link

LSP: Some proof steps are shown twice. #114

Closed kape1395 closed 8 months ago

kape1395 commented 8 months ago

The duplicated steps are visible by holding a cursor for the tooltip to be shown. Probably something with BY <facts> where the facts sometimes are obligations themselves. In some cases, one of those steps remains with the state omitted (e.g FS_Subset part in <4>0. IsFiniteSet(Tx) BY FS_Subset).

This related to #93.

kape1395 commented 8 months ago

Essentially fixed by taking prf_orig instead of prf in the Theorem module unit.