Noted. I didn't define that notation, I just simply pasted in what's in the Coq standard library so it would be clear how the triple constructor worked. Agree

Noted. I didn't define that notation, I just simply pasted in what's in the Coq standard library so it would be clear how the triple constructor worked. Agreed, could use if. I mainly used match with the true/false branches to make it as close to the original Erlang as possible, for readers unfamiliar with the Coq syntax.