Closed wadoon closed 2 months ago
Support of \array2seq and \seq_put (and \seq_upd) in JML (Currently hard coded. It could be better if we add meta-data to functions or have theories)
\array2seq
\seq_put
\seq_upd
Fix \locset(x.*,a[*]), merge with \storeref function
\locset(x.*,a[*])
Tested with the current of the FM tutorial.
Features
Support of
\array2seqand\seq_put(and\seq_upd) in JML (Currently hard coded. It could be better if we add meta-data to functions or have theories)Fix
\locset(x.*,a[*]), merge with \storeref functionTested with the current of the FM tutorial.