Closed
Description
Take this spec:
https://github.com/cosmos/interchain-security/blob/214f6e5c25346b9d3287be8337201f2d15ba538a/tests/mbt/model/ccv.qnt#L337
In particular, this function:
pure def AppendConsumerAddrToPrune(currentState: ProtocolState, oldConsAddr: ConsumerAddr): ProtocolState = {
pure val vscId = currentState.providerState.runningVscId
pure val consumerAddrsToPrune = currentState.providerState.consumerAddrsToPrune
pure val prevConsAddr = consumerAddrsToPrune.get(oldConsAddr).getOrElse(vscId, [])
pure val newConsAddrsToPrune = consumerAddrsToPrune
currentState
}
when I hover over consumerAddrsToPrune, I get this info:
which is not very useful - I want to find the type of consumerAddrsToPrune, which is defined like this:
type ProviderState =
{
[...]
consumerAddrsToPrune: Chain -> VscId -> List[ConsumerAddr],
}
The field curiously also doesn't show up when I hover over providerState
:
It seems this is only broken in this particular function, not everywhere. See how I think it should look, hovering over a providerState somewhere else (red circle for emphasis):
Not sure I'm missing something subtle, or this is a genuine bug.
% quint --version
0.18.0