>function Gcd(a:nat, b:nat) : (g:nat,x:int,y:int))

I hope this is a typo. Otherwise it…requires an unmatched close paren?

That's a new level of cursed syntax.

EDIT: Also, is |array| a common way to get the length of an array in languages? I've never seen that (or some of this other syntax) before and it took me a minute to figure out what was happening.