Show type inference errors in Toolbox's obligation view #434
Description
The spec below causes the TLAPS 1.4.5 SMT back-end to fail to prove the obligation because of a type inference warning (CASE statement). The Toolbox should show type inference warnings not just on the console but also in the obligations view.
---------------------------- MODULE DummyProofs ----------------------------
LOCAL INSTANCE TLAPS
LOCAL INSTANCE Naturals
LOCAL INSTANCE Sequences
Range(f) == { f[x] : x \in DOMAIN f }
IsInjective(s) == \A i, j \in DOMAIN s: (s[i] = s[j]) => (i = j)
----------------------------------------------------------------------------
(* CASE fails to prove with 1.4.5 *)
TailCase(s) == CASE s # << >> -> [i \in 1..(Len(s)-1) |-> s[i+1]]
LEMMA RangeTailCase ==
ASSUME NEW S, NEW ws \in Seq(S), IsInjective(ws)
, ws # <<>>
PROVE \E x \in Range(ws): Range(TailCase(ws)) = Range(ws) \ {x}
BY SMT DEF Range, IsInjective, TailCase
=============================================================================