mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
22 lines
263 B
Plaintext
22 lines
263 B
Plaintext
|
|
||
|
|
module Std
|
||
|
|
|
||
|
|
let halt = any
|
||
|
|
|
||
|
|
let fail { false } = any
|
||
|
|
|
||
|
|
let if (b: bool) (then {b}) (else {not b}) = any
|
||
|
|
|
||
|
|
end
|
||
|
|
|
||
|
|
module List
|
||
|
|
|
||
|
|
use list.List
|
||
|
|
|
||
|
|
let unList < 'a > (l: list 'a)
|
||
|
|
(onCons (h: 'a) (t: list 'a) {l = Cons h t})
|
||
|
|
(onNil {l = Nil})
|
||
|
|
= any
|
||
|
|
|
||
|
|
end
|