Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-09-02 00:37 0b4444ca

View on Github →

feat(pfun/recursion): unbounded recursion (#3778)

Estimated changes

Created src/control/fix.lean

added def roption.fix.approx

added def roption.fix_aux

added theorem roption.fix_def'

Created src/control/lawful_fix.lean

added theorem lawful_fix.fix_eq'

added theorem pi.continuous_curry

added theorem pi.continuous_uncurry

added def pi.monotone_curry

added def pi.monotone_uncurry

added theorem pi.uncurry_curry_continuous

added def roption.fix.approx_chain

added theorem roption.fix.approx_le_fix

added theorem roption.fix.approx_mem_approx_chain

added theorem roption.fix.approx_mono'

added theorem roption.fix.approx_mono

added theorem roption.fix.exists_fix_le_approx

added theorem roption.fix.le_f_of_mem_approx

added theorem roption.fix.mem_iff

added theorem roption.fix_eq

added theorem roption.fix_eq_ωSup

added theorem roption.fix_le

added theorem roption.to_unit_cont

added def roption.to_unit_mono

Created src/data/nat/upto.lean

added def nat.upto.succ

added def nat.upto.zero

added def nat.upto

Modified src/data/pfun.lean

added theorem roption.assert_neg

added theorem roption.assert_pos

added theorem roption.bind_le

added theorem roption.eq_none_or_eq_some

added theorem roption.le_total_of_le_of_le

Modified src/data/sigma/basic.lean

added def sigma.curry

added def sigma.uncurry

Modified src/order/bounded_lattice.lean

Modified src/order/category/Preorder.lean

deleted theorem preorder_hom.coe_id

deleted theorem preorder_hom.coe_inj

deleted def preorder_hom.comp

deleted theorem preorder_hom.comp_id

deleted theorem preorder_hom.ext

deleted def preorder_hom.id

deleted theorem preorder_hom.id_comp

deleted structure preorder_hom

Created src/order/category/omega_complete_partial_order.lean

added def ωCPO.of

added def ωCPO

Created src/order/omega_complete_partial_order.lean

added theorem omega_complete_partial_order.chain.exists_of_mem_map

added def omega_complete_partial_order.chain.map

added theorem omega_complete_partial_order.chain.map_comp

added theorem omega_complete_partial_order.chain.map_id

added theorem omega_complete_partial_order.chain.map_le_map

added theorem omega_complete_partial_order.chain.mem_map

added theorem omega_complete_partial_order.chain.mem_map_iff

added def omega_complete_partial_order.chain.zip

added def omega_complete_partial_order.chain

added theorem omega_complete_partial_order.const_continuous'

added def omega_complete_partial_order.continuous'

added theorem omega_complete_partial_order.continuous.of_bundled'

added theorem omega_complete_partial_order.continuous.of_bundled

added theorem omega_complete_partial_order.continuous.to_bundled

added theorem omega_complete_partial_order.continuous.to_monotone

added def omega_complete_partial_order.continuous

added theorem omega_complete_partial_order.continuous_comp

added theorem omega_complete_partial_order.continuous_hom.bind_continuous'

added theorem omega_complete_partial_order.continuous_hom.coe_apply

added def omega_complete_partial_order.continuous_hom.comp

added theorem omega_complete_partial_order.continuous_hom.comp_assoc

added theorem omega_complete_partial_order.continuous_hom.comp_id

added def omega_complete_partial_order.continuous_hom.const

added theorem omega_complete_partial_order.continuous_hom.const_apply

added theorem omega_complete_partial_order.continuous_hom.continuous

added def omega_complete_partial_order.continuous_hom.flip

added theorem omega_complete_partial_order.continuous_hom.forall_forall_merge'

added theorem omega_complete_partial_order.continuous_hom.forall_forall_merge

added def omega_complete_partial_order.continuous_hom.id

added theorem omega_complete_partial_order.continuous_hom.id_comp

added theorem omega_complete_partial_order.continuous_hom.ite_continuous'

added theorem omega_complete_partial_order.continuous_hom.map_continuous'

added def omega_complete_partial_order.continuous_hom.of_fun

added def omega_complete_partial_order.continuous_hom.of_mono

added def omega_complete_partial_order.continuous_hom.prod.apply

added theorem omega_complete_partial_order.continuous_hom.seq_continuous'

added def omega_complete_partial_order.continuous_hom.to_mono

added theorem omega_complete_partial_order.continuous_hom.ωSup_bind

added theorem omega_complete_partial_order.continuous_hom.ωSup_def

added theorem omega_complete_partial_order.continuous_hom.ωSup_ωSup

added structure omega_complete_partial_order.continuous_hom

added theorem omega_complete_partial_order.continuous_id

added theorem omega_complete_partial_order.id_continuous'

added theorem omega_complete_partial_order.le_ωSup_of_le

added def omega_complete_partial_order.preorder_hom.monotone_apply

added def omega_complete_partial_order.preorder_hom.to_fun_hom

added theorem omega_complete_partial_order.ωSup_le_iff

added theorem omega_complete_partial_order.ωSup_le_ωSup_of_le

added theorem omega_complete_partial_order.ωSup_total

added def pi.monotone_apply

added theorem pi.omega_complete_partial_order.flip₁_continuous'

added theorem pi.omega_complete_partial_order.flip₂_continuous'

added def preorder_hom.bind

added def preorder_hom.const

added def preorder_hom.prod.diag

added def preorder_hom.prod.fst

added def preorder_hom.prod.map

added def preorder_hom.prod.snd

added def preorder_hom.prod.zip

added theorem roption.eq_of_chain

added theorem roption.mem_chain_of_mem_ωSup

added theorem roption.mem_ωSup

added theorem roption.ωSup_eq_none

added theorem roption.ωSup_eq_some

Created src/order/preorder_hom.lean

added theorem preorder_hom.coe_fun_mk

added theorem preorder_hom.coe_id

added theorem preorder_hom.coe_inj

added def preorder_hom.comp

added theorem preorder_hom.comp_id

added theorem preorder_hom.ext

added def preorder_hom.id

added theorem preorder_hom.id_comp

added structure preorder_hom

Created test/general_recursion.lean

added theorem roption.examples.div.cont

added theorem roption.examples.div.equations.eqn_1

added def roption.examples.div.intl

added def roption.examples.div

added theorem roption.examples.easy.cont

added theorem roption.examples.easy.equations.eqn_1

added def roption.examples.easy.intl

added def roption.examples.easy

added def roption.examples.f91'

added theorem roption.examples.f91.cont

added theorem roption.examples.f91.equations.eqn_1

added def roption.examples.f91.intl

added def roption.examples.f91

added theorem roption.examples.f91_dom

added theorem roption.examples.f91_spec'

added theorem roption.examples.f91_spec

added inductive roption.examples.tree

added theorem roption.examples.tree_map'.cont

added theorem roption.examples.tree_map'.equations.eqn_1

added theorem roption.examples.tree_map'.equations.eqn_2

added def roption.examples.tree_map'.intl

added def roption.examples.tree_map'

added theorem roption.examples.tree_map.cont

added theorem roption.examples.tree_map.equations.eqn_1

added theorem roption.examples.tree_map.equations.eqn_2

added def roption.examples.tree_map.intl

added def roption.examples.tree_map