tests/lean/structuralEqns.lean

import Lean

open Lean
open Lean.Meta
def tst (declName : Name) : MetaM Unit := do
  IO.println (← getUnfoldEqnFor? declName)

def foo (xs ys zs : List Nat) : List Nat :=
  match (xs, ys) with
  | (xs', ys')   =>
    match zs with
    | z::zs => foo xs ys zs
    | _ => match ys' with
     | [] => [1]
     | _  => [2]

#eval tst ``foo
#check foo._unfold


def bar (xs ys : List Nat) : List Nat :=
  match xs ++ [], ys ++ [] with
  | xs', ys'   => xs' ++ ys'

#print bar  -- should not contain either `let _discr` aux binding