{:options "--function-syntax:4"}
module TestModule

Test module. More about this test module.

Imports

import J	=	TestModule.MInner`E1
import L	=	TestModule.MInner`E2
import MInner	=	TestModule.MInner`MInner

Submodules

MInner	— Hidden stuff
P
Q
S

Types

class A	— Holds all the state.
class B<Z(0)>
datatype BB<*Q>
codatatype CD<Q>
datatype D<Q>	— Enumeration.
newtype Dup
iterator Gen
newtype Size
type Small	— A small subset type
newtype Smaller	— A brand new type
type SmallS
type SmallW
type T	— A very abstract type.
trait T1<TR>	— A special trait
trait T2
trait T3
type Tint	— A type synonym.
type TQ<Y>
type TTT<!Q(0)>
type WW

Constants

c	:	int	— Number of items.
cc	:	real	— The distance.
ccc	:	bool	— Valid or not.
cccc	:	A	— The internal state.
f1	:	int -> int
f2	:	set<int> ~> seq<int>
f3	:	bool --> TQ<int>
tup0	:	()
tup2	:	(B<real>,set<int>)

Functions

f(r: real, x: int := 0): int	— Returns a constant.
fif(nameonly z: A): A	— return a constant.
lp(): bool	— A copredicate
p(): bool	— Always true.
pf(): bool	— Always true.
pp(older a: A, ghost nameonly x: int): bool
ppp(s: seq<int>, ss: set<A>, mm: map<set<A>,seq<set<A>>>): bool	— Always true.
tf(a: A, new b: A): int	— A two-state function

Methods

bump(i: int) returns (j: int)	— increments input
ModifyA(a: A)
zero() returns (z: int)	— Sets to zero.

Lemmas

IsX()	— always true
TS()