Return to Answer

deleted 11 characters in body

Source Link

edited Oct 17, 2021 at 13:38

Lean, 211211 205 bytes

Helper:

inductivenotation R
|c`L`:list=list ℕ->ℕ->list
structure R:=m::(A:L)(B:ℕ->R)(C:L)
def r:list ℕL->list ℕ>L->ℕ->R
|_[]_:=R.c[]0[]
|p(h::t)0:=R.cm p h t
|p(h::t)(n+1):=r(p++[h])t n
|_[]_:=R.m[]0[]

Actual function:

λl a b,let(R.c f x l):=r[]l a,(R.c m y z):=r[]l=r[]f.C(b-a-1)in f++yf.A++z.B::m++xz.A++f.B::z.C

Try it online!Try it online!

There's got to be a way to make product types and define type aliases easily, but I couldn't find it.

Lean, 211 bytes

Helper:

inductive R
|c:list ℕ->ℕ->list ℕ->R
def r:list ℕ->list ℕ->ℕ->R
|_[]_:=R.c[]0[]
|p(h::t)0:=R.c p h t
|p(h::t)(n+1):=r(p++[h])t n

Actual function:

λl a b,let(R.c f x l):=r[]l a,(R.c m y z):=r[]l(b-a-1)in f++y::m++x::z

Try it online!

There's got to be a way to make product types and define type aliases easily, but I couldn't find it.

Lean, 211 205 bytes

Helper:

notation `L`:=list ℕ
structure R:=m::(A:L)(B:ℕ)(C:L)
def r:L->L->ℕ->R
|p(h::t)0:=R.m p h t
|p(h::t)(n+1):=r(p++[h])t n
|_[]_:=R.m[]0[]

Actual function:

λl a b,let f:=r[]l a,z:=r[]f.C(b-a-1)in f.A++z.B::z.A++f.B::z.C

Try it online!

There's got to be a way to make product types and define type aliases easily, but I couldn't find it.

Source Link

created Oct 16, 2021 at 22:58

user

Lean, 211 bytes

Helper:

inductive R
|c:list ℕ->ℕ->list ℕ->R
def r:list ℕ->list ℕ->ℕ->R
|_[]_:=R.c[]0[]
|p(h::t)0:=R.c p h t
|p(h::t)(n+1):=r(p++[h])t n

Actual function:

λl a b,let(R.c f x l):=r[]l a,(R.c m y z):=r[]l(b-a-1)in f++y::m++x::z

Try it online!

There's got to be a way to make product types and define type aliases easily, but I couldn't find it.