Entry Value
Package Name option-thm
Count 3
Theorems
  • option_cases : !x. x = NONE \/ (?a. x = SOME a)
  • option_distinct : !a. ~(SOME a = NONE)
  • option_inj : !a b. SOME a = SOME b <=> a = b
  • Back to main package page