Entry	Value
Package Name	option-def
Count	2
Theorems	option_INDUCT : !p. p NONE /\ (!a. p (SOME a)) ==> (!x. p x) option_RECURSION : !b f. ?fn. fn NONE = b /\ (!a. fn (SOME a) = f a)

Back to main package page