Theory "basicSize"

Parents     option   numeral

Signature

Constant Type
bool_size :bool -> num
one_size :unit -> num
option_size :(α -> num) -> α option -> num
pair_size :(α -> num) -> (β -> num) -> α # β -> num
sum_size :(α -> num) -> (β -> num) -> α + β -> num

Definitions

bool_size_def 
|- ∀b. bool_size b = 0
pair_size_def 
|- ∀f g. pair_size f g = (λ(x,y). f x + g y)
one_size_def 
|- ∀x. one_size x = 0
sum_size_def 
|- (∀f g x. sum_size f g (INL x) = f x) ∧ ∀f g y. sum_size f g (INR y) = g y
option_size_def 
|- (∀f. option_size f NONE = 0) ∧ ∀f x. option_size f (SOME x) = SUC (f x)