Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-05-21 11:44 f0bcba56

View on Github →

feat(computability/partrec_code): Kleene normal form theorem among other things

Estimated changes

added theorem guard_false
added theorem guard_true
added theorem computable.cond
added theorem computable.encode_iff
added theorem computable.list_append
added theorem computable.list_concat
added theorem computable.list_cons
added theorem computable.list_length
added theorem computable.list_nth
added theorem computable.nat_bodd
added theorem computable.nat_cases
added theorem computable.nat_div2
added theorem computable.option_bind
added theorem computable.option_map
added theorem computable.option_some
added theorem computable.pred
added theorem computable.succ
added theorem computable.sum_cases
added theorem computable.sum_inl
added theorem computable.sum_inr
added theorem computable.unpair
deleted theorem nat.partrec.code.rec_prim
deleted inductive nat.partrec.code
deleted theorem nat.partrec.rfind'
added theorem partrec.fix
added theorem partrec.sum_cases_left
added inductive nat.partrec.code
added theorem nat.partrec.rfind'
added theorem primrec.list_range
added theorem primrec.nat_max
added theorem primrec.nat_min
added theorem primrec.option_is_some
added theorem option.bind_eq_some'
added theorem option.guard_eq_some'
added theorem option.map_eq_some'
added theorem option.none_bind'
added theorem option.some_bind'
added theorem pfun.fix_induction
modified theorem pfun.mem_fix_iff
added theorem roption.bind_dom
added theorem roption.mem_coe