Commit 2023-04-20 10:27 ac0e585f

View on Github →

feat: port Data.Seq.Parallel (#3512) This PR also make Prod.rec computable.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Seq/Parallel.lean

added theorem Computation.exists_of_mem_parallel

added theorem Computation.map_parallel

added theorem Computation.mem_parallel

added def Computation.parallel.aux1

added def Computation.parallel.aux2

added def Computation.parallel

added def Computation.parallelRec

added theorem Computation.parallel_congr_left

added theorem Computation.parallel_congr_lem

added theorem Computation.parallel_congr_right

added theorem Computation.parallel_empty

added theorem Computation.parallel_promises

added theorem Computation.terminates_parallel.aux

added theorem Computation.terminates_parallel

Modified Mathlib/Init/Data/Prod.lean

added def Prod.recC

added theorem rec_eq_recC