original.name="Record_Valid_2"
======
>>> main.whiley
type Point is { int x, int y }
type Position is { int x, int y }

function fromXY(int x, int y) -> (Position r)
ensures r.x == x && r.y == y:
    return Point{x:x, y:y}

public export method test():
    Position p = fromXY(1,2)
    //
    assert p.x == 1 && p.y == 2
---