Get value in the statics of ATS¶

Todo

organize

ATS-Postiats/prelude/basics_dyn.sats

dataprop
EQINT (int, int) = {x: int} EQINT (x, x)
//
extern prfun eqint_make {x,y:int | x == y} (): EQINT (x, y)
//
extern prfun
eqint_make_gint
  {tk:tk}{x:int} (x: g1int (tk, x)): [y: int] EQINT (x, y)

fun goo {x:int | x == 1} (): void = ()

fun foo (): void = let
  val x = 1
  val [y:int] EQINT () = eqint_make_gint (x)
in
  goo {y} ()
end