Leo Freitas

@nickbattle not yet. Guess now with my much clearer understanding of the visitors, shouldn\'t be too hard. I am focusing on the proof strategies atm, but eventually such calculations would...

Yes.

Creating the launch is somewhat straightforward. Tasks are more sophisticated. Only needed tasks for ANTLR complications. And create launch as needed. Nick’s right that they may get stale and hard...

I use this task to clear the VSCode cache, which is important in some circumstances for ANTLR - Ie for any tool that generates code in the development sources to...

If you look at the launch.json in VDMToolkit plugins/vdm2isa/.vscode/launch.json you will see various launch confit for debugging VDMJ itself. This also works for lsp plugins/vdm2isa-lsp/.vscode/launch.json In fact, if you look...

@mortenhaahr don't think I have your email, so will make a comment here (for Nick as well, whom I do have the email!) :-), about the Chess game. I've ported...

Hi Nick, I considered that as well (i.e. be a VDM_Toolkit thing). But then I realised that VDM has measures for functions, but not for loops/operations. In the case of...

Hi, It’s the console. So the scenario is this: 1) have my model correctly type checked etc. if running in the console, all works fine 2) I now want to...