Switch branches/tags
Nothing to show
Find file History
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
..
Failed to load latest commit information.
.gitignore
Makefile
README.md
main.c
main.dats
rps.dats
rps.sats

README.md

Rock-paper-scissors library

Purpose

To learn statics and proofs on ATS language.

How to use

implement main0 () = {
  (* Proofs *)
  val paper_p = p_rps_t()
  val (pf_win | win_p) = rps_win_p (paper_p)
  val () = println! (win_p, " win ", paper_p, ".") // => Scissors win Paper.
  val (_, _ | even_p) = rps_even_p (pf_win | win_p, paper_p)
  val () = println! (even_p, " is even between ", win_p, " and ", paper_p, ".") // => Rock is even between Scissors and Paper.
  (* Statics *)
  val paper_s = p_rps_t()
  val win_s = rps_win_s (paper_s)
  val () = println! (win_s, " win ", paper_s, ".") // => Scissors win Paper.
  val even_s = rps_even_s (win_s, paper_s)
  val () = println! (even_s, " is even between ", win_s, " and ", paper_s, ".") // => Rock is even between Scissors and Paper.
}

The rps_win_p and rps_win_s function returns a value that wins the argument. The rps_even_p and rps_even_s function returns a value that is even between the arguments. ATS language prove these functions, with proof function and static function.

Question

  • Can't use static function instead of proofs? => Yes, can use it as statics function.

Discussions