Show type inference errors in Toolbox's obligation view

[lemmy]

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

=============================================================================

[lemmy]

@ahelwer FYI