I probably should look more closely at Agda. But the if_then_else_ example is basically smalltalk equivalant - although I suspect Agda will be able to do witho

I probably should look more closely at Agda. But the if_then_else_ example is basically smalltalk equivalant - although I suspect Agda will be able to do without the angle brackets that Smalltalk often needs in these cases.