Nathan Taylor
Nathan Taylor
At present, one can't compile, for instance, an ivy file named `time.ivy`: ``` (venv) ➜ accord_ivy git:(main) ✗ cat walltime.ivy #lang ivy1.8 # Some functionality for timestamp operations. include collections...
Given the following simplified code: ``` 123 class man_msg_t = { 124 action handle(self: manager_id, ^msg: man_msg_t) 125 } 126 ... 154 155 # An unpark message is sent to...
On commit `6f081c8c93` I'm observing an assertion failure in `tcp_test`: ``` ➜ sandbox git:(main) ✗ ~/bin/ivyc target=test echo.ivy && ivy_launch cid=1 sid=1 echo g++ -Wno-parentheses-equality -std=c++11 -I /Users/ntaylor/code/ivy/ivy/include -L /Users/ntaylor/code/ivy/ivy/lib...
Currently, when ivy_to_cpp-generated code prints out the current model, it doesn't emit a trailing newline. This makes the output slightly tricky to read: consider the following example: ``` 99 (define-fun...
I'm writing an Ivy specification which attempted to partially initialise a relation in an `after init` block. Here's a distillation of the intention: ``` #lang ivy1.8 type range_t = {0..max}...
Whilst trying to compile the following (incorrect) assertion: ``` 96 ensure forall P1:pid,P2:pid,I. msg_count = 0 -> 97 host(P1).contents.end = host(P2).contents.end & 98 (I < host(P1).contents.end -> host(P1).contents.value(I) = host(P2).contents.value(I));...
While working on the Vim syntax plugin[1], I noticed that the Emacs major mode was missing a few (presumably recently-added) reserved words. This patch synchronises the major mode's list of...
Dear all, In Propositions and Proofs, when the `suffices` keyword is introduced, the text reads, "Writing ``suffices hq : q`` leaves us with two goals.". I was expecting, in the...
Defining the `Implies` function whilst hiding it from the rendered document makes following the chapter difficult, as the reader expects that it is a built-in alongside the other propositional connectives....