Addition to Manual: elif construction with pipe

[martin-d2]

Hi Galois! :-)

Sorry if this is the wrong place for requests for the manual.

I encountered the following code:

state = 
 if foo then bar
  | foo2 then bar2
  | foo3 then bar3
  else bar4

where it wasn't clear that the pipe was an extension of elif or similar. Grepping through the manual didn't produce anything apart from scratching of heads, even though I was certain it was a different usage to || for logical OR, and the 'such that' comprehension notation in e.g. [f x | x <- xs].

Really sorry if it's a common construction or usage, but neither my colleague or I had come across it before: would you be able to add this to the manual? I think very minimal (if any) explanation will be needed.

Thanks!

Martin

[weaversa]

There is some documentation here that could make it’s way into the manual: https://github.com/GaloisInc/cryptol/blob/master/docs/Syntax.md#multi-way-conditionals

[martin-d2]

That's perfect, thanks @weaversa! Didn't know this document existed.

[weaversa]

Well then, I also highly recommend the Cryptol primitives and module system docs in the same directory. 😁

[atomb]

Yep, we should really add this to the manual. Thanks for pointing it out!

[robdockins]

The syntax document is actually already incorporated into the book as appendix F. Section F.9, in particular, discusses multi-way if.