repo.or.cz
/
why3.git
/
blob
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
log
|
graphiclog1
|
graphiclog2
|
commit
|
commitdiff
|
tree
|
refs
|
edit
|
fork
blame
|
history
|
raw
|
HEAD
Merge branch 'knuth-bubble-sort' into 'master'
[why3.git]
/
examples
/
bts
/
138.mlw
blob
db43286293526df67b281063ab47a4dba4267d42
1
module Test
2
3
use int.Int
4
5
type a = < range 22 46 >
6
7
let f (b : a) =
8
requires {a'int b = 42}
9
ensures {a'int result = a'int b}
10
(42:a)
11
12
end
13
14
module Test1
15
clone Test as T (* Replace with Test does not work *)
16
17
end