| (some _private.structuralEqns.0.foo._unfold) | |
| foo._unfold (xs ys zs : List Nat) : | |
| foo xs ys zs = | |
| match (xs, ys) with | |
| | (xs', ys') => | |
| match zs with | |
| | z :: zs => foo xs ys zs | |
| | x => | |
| match ys' with | |
| | [] => [1] | |
| | x => [2] | |
| def bar : List Nat → List Nat → List Nat := | |
| fun xs ys => | |
| match xs ++ [], ys ++ [] with | |
| | xs', ys' => xs' ++ ys' |