Entry Value
Package Name sum-def
Count 10
Theorems
  • ISL_INL : !a. ISL (INL a)
  • ISL_INR : !b. ~ISL (INR b)
  • ISR_INL : !a. ~ISR (INL a)
  • ISR_INR : !b. ISR (INR b)
  • OUTL : !a. OUTL (INL a) = a
  • OUTR : !b. OUTR (INR b) = b
  • case_sum_left : !f g a. case_sum f g (INL a) = f a
  • case_sum_right : !f g b. case_sum f g (INR b) = g b
  • sum_INDUCT : !p. (!a. p (INL a)) /\ (!b. p (INR b)) ==> (!x. p x)
  • sum_RECURSION : !f g. ?fn. (!a. fn (INL a) = f a) /\ (!b. fn (INR b) = g b)
  • Back to main package page