Commit 2018-05-17 04:23 e017f0f1

View on Github →

feat(data/computability): primrec, denumerable

Estimated changes

modified theorem bool.cond_ff
added theorem bool.cond_to_bool
modified theorem bool.cond_tt
added theorem bool.to_bool_and
added theorem bool.to_bool_not
added theorem bool.to_bool_or
added def nat.cases
added theorem nat.cases_succ
added theorem nat.cases_zero
added def nat.elim
added theorem nat.elim_succ
added theorem nat.elim_zero
added theorem nat.primrec.add
added theorem nat.primrec.cases1
added theorem nat.primrec.cases
added theorem nat.primrec.const
added theorem nat.primrec.mul
added theorem nat.primrec.of_eq
added theorem nat.primrec.pow
added theorem nat.primrec.prec1
added theorem nat.primrec.pred
added theorem nat.primrec.sub
added theorem nat.primrec.swap'
added inductive nat.primrec
added def nat.unpaired
added theorem primrec.comp
added theorem primrec.comp₂
added theorem primrec.cond
added theorem primrec.const
added theorem primrec.dom_bool
added theorem primrec.dom_bool₂
added theorem primrec.dom_fintype
added theorem primrec.encdec
added theorem primrec.encode_iff
added theorem primrec.fst
added theorem primrec.ite
added theorem primrec.list_index_of
added theorem primrec.list_inth
added theorem primrec.list_nth
added theorem primrec.map_decode_iff
added theorem primrec.nat_add
added theorem primrec.nat_bit0
added theorem primrec.nat_bit1
added theorem primrec.nat_bit
added theorem primrec.nat_bodd
added theorem primrec.nat_bodd_div2
added theorem primrec.nat_cases'
added theorem primrec.nat_cases1
added theorem primrec.nat_cases
added theorem primrec.nat_div2
added theorem primrec.nat_div
added theorem primrec.nat_div_mod
added theorem primrec.nat_elim'
added theorem primrec.nat_elim1
added theorem primrec.nat_elim
added theorem primrec.nat_iff
added theorem primrec.nat_le
added theorem primrec.nat_mod
added theorem primrec.nat_mul
added theorem primrec.nat_sub
added theorem primrec.of_eq
added theorem primrec.of_nat_iff
added theorem primrec.option_bind1
added theorem primrec.option_bind
added theorem primrec.option_cases
added theorem primrec.option_iget
added theorem primrec.option_map1
added theorem primrec.option_map
added theorem primrec.option_some
added theorem primrec.pair
added theorem primrec.pred
added theorem primrec.snd
added theorem primrec.succ
added theorem primrec.unpair
added def primrec
added theorem primrec_pred.comp
added theorem primrec_pred.of_eq
added def primrec_pred
added theorem primrec_rel.comp
added theorem primrec_rel.comp₂
added theorem primrec_rel.of_eq
added def primrec_rel
added theorem primrec₂.comp
added theorem primrec₂.comp₂
added theorem primrec₂.const
added theorem primrec₂.curry
added theorem primrec₂.encode_iff
added theorem primrec₂.left
added theorem primrec₂.mkpair
added theorem primrec₂.nat_iff'
added theorem primrec₂.nat_iff
added theorem primrec₂.of_eq
added theorem primrec₂.of_nat_iff
added theorem primrec₂.right
added theorem primrec₂.swap
added theorem primrec₂.uncurry
added theorem primrec₂.unpaired'
added theorem primrec₂.unpaired
added def primrec₂
added theorem finset.attach_map_val
added def finset.map
added theorem finset.map_empty
added theorem finset.map_eq_empty
added theorem finset.map_eq_image
added theorem finset.map_filter
added theorem finset.map_insert
added theorem finset.map_inter
added theorem finset.map_map
added theorem finset.map_refl
added theorem finset.map_singleton
added theorem finset.map_subset_map
added theorem finset.map_to_finset
added theorem finset.map_union
added theorem finset.map_val
added theorem finset.mem_map
added theorem finset.mem_map_of_mem
added theorem finset.sort_sorted_lt
added theorem list.filter_congr
added theorem list.foldl_ext
added theorem list.foldr_ext
added theorem list.map_add_range'
added theorem list.nth_le_map'
added theorem list.nth_le_map
added theorem list.nth_map
added theorem list.pairwise.and
added theorem list.pairwise.imp₂
added theorem list.range_succ_eq_map
added theorem list.reverse_range'