blob: c9c27b5d827a10cd2c46507117dbb34d75b8171e (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
|
default Order dec
$include <flow.sail>
$include <arith.sail>
val f : forall 'n, 'n >= 0. atom(8 * 'n) -> int
function f(x) = x+1
val g : forall 'n, 'n > 0. atom('n) -> atom(2*'n)
val h : forall 'n, 'n > 1. atom('n) -> int
function h(x) = x
val test : unit -> bool
function test() = {
/* Using f with Coq would need us to provide/infer witnesses for 'n
f(0) == 1 & f(8) == 9
*/
h(g(1)) == 2
}
|
