whiley_test_file 0.6.2

original.name="RecursiveType_Valid_20"
boogie.ignore=true
Whiley2Boogie.issue=79
======
>>> main.whiley


type nat is int

type pos is int

type expr is nat | {expr rhs, expr lhs}

type posExpr is pos | {posExpr rhs, posExpr lhs}

function f(posExpr e1) -> expr:
    expr e2 = e1
    return e2

public export method test() :
    expr e = f({rhs: 1, lhs: {rhs: 2, lhs: 1}})
    assume e == {lhs:{lhs:1,rhs:2},rhs:1}


---