Type

type-t

Description

Maybe type constructor. (maybe-t A) represents a value of type A that may or may not exist.

Definition

(define-enum (maybe-t A)
  (just (value A))
  (nothing))

Generated

(claim just  (all (A) (-> A (maybe-t A))))
(claim is-just (all (A) (-> (maybe-t A) bool-t)))
(claim just-value (all (A) (-> (maybe-t A) A)))
(claim just-put-value (all (A) (-> (maybe-t A) A void-t)))

(claim nothing (all (A) (-> (maybe-t A))))
(claim is-nothing (all (A) (-> (maybe-t A) bool-t)))

Examples

(define x (just 42))
(is-just x)          ;; => true
(is-nothing x)       ;; => false
(just-value x)     ;; => 42