Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-05-18 05:14 38d55369

View on Github →

feat(computability/partrec): starting work on partial recursive funcs

Estimated changes

Created data/computability/partrec.lean

added theorem nat.partrec.of_eq

added theorem nat.partrec.prim

added inductive nat.partrec

Modified data/computability/primrec.lean

modified def nat.unpaired

Modified data/pfun.lean

added def pfun.bind

added theorem pfun.coe_val

added def pfun.ext'

added def pfun.ext

added theorem pfun.lift_eq_coe

added def pfun.map

added def roption.bind

added theorem roption.bind_eq_bind

added theorem roption.bind_some

deleted theorem roption.eq_ret_of_mem

added theorem roption.eq_some_of_mem

deleted theorem roption.exists_of_mem_bind

added def roption.ext'

added def roption.ext

added def roption.map

added theorem roption.map_eq_map

added theorem roption.map_some

added theorem roption.mem_bind_iff

added theorem roption.mem_map

added theorem roption.mem_map_iff

added theorem roption.mem_of_option

deleted theorem roption.mem_ret

deleted theorem roption.mem_ret_iff

modified theorem roption.mem_some

added theorem roption.mem_some_iff

added theorem roption.mem_to_option

added def roption.none

modified theorem roption.of_to_option

added theorem roption.ret_eq_some

added def roption.some

deleted theorem roption.some_bind

modified theorem roption.to_of_option