789d4e148f
This step packs a collection of mutually recursive functions into a single one. We use `psum` to combine the different domains, and `psum.cases_on` to combine the codomains.
27 lines
712 B
Text
27 lines
712 B
Text
import data.vector
|
||
open nat
|
||
universes u v
|
||
set_option pp.all true
|
||
|
||
set_option trace.eqn_compiler.wf_rec true
|
||
set_option trace.debug.eqn_compiler.wf_rec true
|
||
set_option trace.debug.eqn_compiler.mutual true
|
||
set_option trace.eqn_compiler.elim_match true
|
||
|
||
|
||
mutual def even, odd
|
||
with even : nat → bool
|
||
| 0 := tt
|
||
| (a+1) := odd a
|
||
with odd : nat → bool
|
||
| 0 := ff
|
||
| (a+1) := even a
|
||
|
||
|
||
mutual def f, g {α : Type u} {β : Type v} (f : α → β) (p : α × β)
|
||
with f : Π n : nat, vector (α × β) n
|
||
| 0 := vector.nil
|
||
| (succ n) := vector.cons p $ (g n p.1).map (λ b, (p.1, b))
|
||
with g : Π n : nat, α → vector β n
|
||
| 0 a := vector.nil
|
||
| (succ n) a := vector.cons p.2 $ (f n).map (λ p, p.2)
|