Commit 2023-04-20 06:30 133aee55

View on Github →

feat: port Data.Seq.WSeq (#3405) This PR also make Option.recOn computable.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/Option/Basic.lean

added def Option.recOnC.{u_1,

added theorem Option.recOn_eq_recOnC

Created Mathlib/Data/Seq/WSeq.lean

added theorem Stream'.WSeq.BisimO.imp

added def Stream'.WSeq.BisimO

added theorem Stream'.WSeq.Equiv.equivalence

added theorem Stream'.WSeq.Equiv.ext

added theorem Stream'.WSeq.Equiv.refl

added theorem Stream'.WSeq.Equiv.symm

added theorem Stream'.WSeq.Equiv.trans

added def Stream'.WSeq.Equiv

added theorem Stream'.WSeq.LiftRel.equiv

added theorem Stream'.WSeq.LiftRel.refl

added theorem Stream'.WSeq.LiftRel.swap

added theorem Stream'.WSeq.LiftRel.swap_lem

added theorem Stream'.WSeq.LiftRel.symm

added theorem Stream'.WSeq.LiftRel.trans

added def Stream'.WSeq.LiftRel

added theorem Stream'.WSeq.LiftRelO.imp

added theorem Stream'.WSeq.LiftRelO.imp_right

added theorem Stream'.WSeq.LiftRelO.swap

added def Stream'.WSeq.LiftRelO

added def Stream'.WSeq.all

added def Stream'.WSeq.any

added def Stream'.WSeq.append

added theorem Stream'.WSeq.append_assoc

added theorem Stream'.WSeq.append_nil

added def Stream'.WSeq.bind

added theorem Stream'.WSeq.bind_assoc

added theorem Stream'.WSeq.bind_congr

added theorem Stream'.WSeq.bind_ret

added def Stream'.WSeq.collect

added def Stream'.WSeq.compute

added def Stream'.WSeq.cons

added theorem Stream'.WSeq.cons_append

added theorem Stream'.WSeq.cons_congr

added def Stream'.WSeq.destruct

added def Stream'.WSeq.destruct_append.aux

added theorem Stream'.WSeq.destruct_append

added theorem Stream'.WSeq.destruct_congr

added theorem Stream'.WSeq.destruct_congr_iff

added theorem Stream'.WSeq.destruct_cons

added theorem Stream'.WSeq.destruct_dropn

added theorem Stream'.WSeq.destruct_flatten

added def Stream'.WSeq.destruct_join.aux

added theorem Stream'.WSeq.destruct_join

added theorem Stream'.WSeq.destruct_map

added theorem Stream'.WSeq.destruct_nil

added theorem Stream'.WSeq.destruct_ofSeq

added theorem Stream'.WSeq.destruct_some_of_destruct_tail_some

added theorem Stream'.WSeq.destruct_tail

added theorem Stream'.WSeq.destruct_terminates_of_get?_terminates

added theorem Stream'.WSeq.destruct_think

added def Stream'.WSeq.drop.aux

added theorem Stream'.WSeq.drop.aux_none

added def Stream'.WSeq.drop

added theorem Stream'.WSeq.dropn_add

added theorem Stream'.WSeq.dropn_congr

added theorem Stream'.WSeq.dropn_cons

added theorem Stream'.WSeq.dropn_nil

added theorem Stream'.WSeq.dropn_ofSeq

added theorem Stream'.WSeq.dropn_tail

added theorem Stream'.WSeq.dropn_think

added theorem Stream'.WSeq.eq_or_mem_iff_mem

added theorem Stream'.WSeq.exists_dropn_of_mem

added theorem Stream'.WSeq.exists_get?_of_mem

added theorem Stream'.WSeq.exists_of_liftRel_left

added theorem Stream'.WSeq.exists_of_liftRel_right

added theorem Stream'.WSeq.exists_of_mem_bind

added theorem Stream'.WSeq.exists_of_mem_join

added theorem Stream'.WSeq.exists_of_mem_map

added def Stream'.WSeq.filter

added def Stream'.WSeq.filterMap

added def Stream'.WSeq.find

added def Stream'.WSeq.findIndex

added def Stream'.WSeq.findIndexes

added def Stream'.WSeq.flatten

added theorem Stream'.WSeq.flatten_congr

added theorem Stream'.WSeq.flatten_equiv

added theorem Stream'.WSeq.flatten_pure

added theorem Stream'.WSeq.flatten_think

added def Stream'.WSeq.get

added def Stream'.WSeq.get?

added theorem Stream'.WSeq.get?_add

added theorem Stream'.WSeq.get?_congr

added theorem Stream'.WSeq.get?_mem

added theorem Stream'.WSeq.get?_ofSeq

added theorem Stream'.WSeq.get?_tail

added theorem Stream'.WSeq.get?_terminates_le

added def Stream'.WSeq.head

added theorem Stream'.WSeq.head_congr

added theorem Stream'.WSeq.head_cons

added theorem Stream'.WSeq.head_nil

added theorem Stream'.WSeq.head_ofSeq

added theorem Stream'.WSeq.head_some_of_get?_some

added theorem Stream'.WSeq.head_some_of_head_tail_some

added theorem Stream'.WSeq.head_terminates_iff

added theorem Stream'.WSeq.head_terminates_of_get?_terminates

added theorem Stream'.WSeq.head_terminates_of_head_tail_terminates

added theorem Stream'.WSeq.head_terminates_of_mem

added theorem Stream'.WSeq.head_think

added def Stream'.WSeq.indexOf

added def Stream'.WSeq.indexesOf

added def Stream'.WSeq.inits

added def Stream'.WSeq.isEmpty

added def Stream'.WSeq.join

added theorem Stream'.WSeq.join_append

added theorem Stream'.WSeq.join_congr

added theorem Stream'.WSeq.join_cons

added theorem Stream'.WSeq.join_join

added theorem Stream'.WSeq.join_map_ret

added theorem Stream'.WSeq.join_nil

added theorem Stream'.WSeq.join_ret

added theorem Stream'.WSeq.join_think

added def Stream'.WSeq.length

added theorem Stream'.WSeq.length_eq_map

added theorem Stream'.WSeq.liftRel_append

added theorem Stream'.WSeq.liftRel_bind

added theorem Stream'.WSeq.liftRel_cons

added theorem Stream'.WSeq.liftRel_destruct

added theorem Stream'.WSeq.liftRel_destruct_iff

added theorem Stream'.WSeq.liftRel_dropn_destruct

added theorem Stream'.WSeq.liftRel_flatten

added theorem Stream'.WSeq.liftRel_join.lem

added theorem Stream'.WSeq.liftRel_join

added theorem Stream'.WSeq.liftRel_map

added theorem Stream'.WSeq.liftRel_nil

added theorem Stream'.WSeq.liftRel_think_left

added theorem Stream'.WSeq.liftRel_think_right

added def Stream'.WSeq.map

added theorem Stream'.WSeq.map_append

added theorem Stream'.WSeq.map_comp

added theorem Stream'.WSeq.map_congr

added theorem Stream'.WSeq.map_cons

added theorem Stream'.WSeq.map_id

added theorem Stream'.WSeq.map_join

added theorem Stream'.WSeq.map_nil

added theorem Stream'.WSeq.map_ret

added theorem Stream'.WSeq.map_think

added theorem Stream'.WSeq.mem_append_left

added theorem Stream'.WSeq.mem_congr

added theorem Stream'.WSeq.mem_cons

added theorem Stream'.WSeq.mem_cons_iff

added theorem Stream'.WSeq.mem_cons_of_mem

added theorem Stream'.WSeq.mem_map

added theorem Stream'.WSeq.mem_of_mem_dropn

added theorem Stream'.WSeq.mem_of_mem_tail

added theorem Stream'.WSeq.mem_rec_on

added theorem Stream'.WSeq.mem_think

added def Stream'.WSeq.nil

added theorem Stream'.WSeq.nil_append

added theorem Stream'.WSeq.not_mem_nil

added def Stream'.WSeq.ofList

added theorem Stream'.WSeq.ofList_cons

added theorem Stream'.WSeq.ofList_nil

added def Stream'.WSeq.ofSeq

added def Stream'.WSeq.ofStream

added theorem Stream'.WSeq.of_mem_append

added theorem Stream'.WSeq.productive_congr

added theorem Stream'.WSeq.productive_iff

added def Stream'.WSeq.recOn

added def Stream'.WSeq.removeNth

added def Stream'.WSeq.ret

added theorem Stream'.WSeq.ret_bind

added def Stream'.WSeq.scanl

added theorem Stream'.WSeq.seq_destruct_cons

added theorem Stream'.WSeq.seq_destruct_nil

added theorem Stream'.WSeq.seq_destruct_think

added def Stream'.WSeq.splitAt

added def Stream'.WSeq.tail.aux

added def Stream'.WSeq.tail

added theorem Stream'.WSeq.tail_congr

added theorem Stream'.WSeq.tail_cons

added theorem Stream'.WSeq.tail_nil

added theorem Stream'.WSeq.tail_ofSeq

added theorem Stream'.WSeq.tail_think

added def Stream'.WSeq.take

added def Stream'.WSeq.think

added theorem Stream'.WSeq.think_append

added theorem Stream'.WSeq.think_congr

added theorem Stream'.WSeq.think_equiv

added theorem Stream'.WSeq.toList'_cons

added theorem Stream'.WSeq.toList'_map

added theorem Stream'.WSeq.toList'_nil

added theorem Stream'.WSeq.toList'_think

added def Stream'.WSeq.toList

added theorem Stream'.WSeq.toList_cons

added theorem Stream'.WSeq.toList_nil

added theorem Stream'.WSeq.toList_ofList

added def Stream'.WSeq.toSeq

added theorem Stream'.WSeq.toSeq_ofSeq

added def Stream'.WSeq.union

added def Stream'.WSeq.updateNth

added def Stream'.WSeq.zip

added def Stream'.WSeq.zipWith

added def Stream'.WSeq