Commit 3b76a906 authored by François Bobot's avatar François Bobot

[Stdlib] Peano: allows to convert to int63 using partial

parent 9d25d06b
(** {2 Peano arithmetic}
This module implements the idea described in this paper:
......@@ -101,3 +100,12 @@ module MinMax
ensures { result.v = min x.v y.v }
module Int63
use Peano
val partial to_int63 (x:t) : int63
ensures { result = x.v }
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment