mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
22 lines
416 B
Plaintext
22 lines
416 B
Plaintext
|
module RecursiveRecord
|
||
|
|
use mach.java.util.NoSuchElementException
|
||
|
|
use mach.java.util.Optional
|
||
|
|
|
||
|
|
|
||
|
|
type t = {
|
||
|
|
a : bool;
|
||
|
|
next : optional t
|
||
|
|
}
|
||
|
|
|
||
|
|
let get_next (self : t) : t
|
||
|
|
ensures { self.next = Optional.build result }
|
||
|
|
raises { NoSuchElementException.E -> not is_present self.next }
|
||
|
|
=
|
||
|
|
Optional.get self.next
|
||
|
|
|
||
|
|
let default_cstr [@java:constructor]() = { a = false; next = empty () }
|
||
|
|
|
||
|
|
end
|
||
|
|
|
||
|
|
|