feat: port Data.Seq.WSeq (#3405)

This PR also make `Option.recOn` computable.



Co-authored-by: Pol_tta <52843868+Komyyy@users.noreply.github.com>
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Mathlib.lean

@@ -1076,6 +1076,7 @@ import Mathlib.Data.Rel
 import Mathlib.Data.Semiquot
 import Mathlib.Data.Seq.Computation
 import Mathlib.Data.Seq.Seq
+import Mathlib.Data.Seq.WSeq
 import Mathlib.Data.Set.Accumulate
 import Mathlib.Data.Set.Basic
 import Mathlib.Data.Set.BoolIndicator

Mathlib/Data/Option/Basic.lean

@@ -379,7 +379,17 @@ lemma rec_eq_recC : @Option.rec = @Option.recC := by
   | none => rfl
   | some a =>
     rw [Option.recC]
-
+
+/-- A computable version of `Option.recOn`. Workaround until Lean has native support for this. -/
+def recOnC.{u_1, u} {α : Type u} {motive : Option α → Sort u_1}
+    (t : Option α) (none : motive none) (some : (val : α) →  motive (some val)) : motive t :=
+  Option.recC none some t
+
+@[csimp]
+lemma recOn_eq_recOnC : @Option.recOn = @Option.recOnC := by
+  ext α motive o none some
+  rw [Option.recOn, rec_eq_recC, Option.recOnC]
+
 end recursor_workarounds
 
 theorem orElse_eq_some (o o' : Option α) (x : α) :