QSort.hss

flatten-module
consider 'qsort
ww-split-param 1 [|wrap|] [|unwrap|]
bash
{consider lam ; alpha-lam 't}
any-call (unfold 'wrap)
any-call (unfold 'unwrap)
simplify
{rhs-of 'work
  alpha-lam 'xs
  any-td case-float-arg
  0
  eta-expand 'acc
  bash
  {consider case ; consider case ; consider alt
     alpha-alt ['bs,'cs]
     any-td (unfold-rule "repH ++")
     any-bu case-float-arg
     simplify
     one-td (foreward (ww-fusion [| absH t |] [| repH t |] [| work bs |]))
     one-td (foreward (ww-fusion [| absH t |] [| repH t |] [| work cs |]))
     any-call (unfold-rule "repH (:)")
     simplify
  }
  any-call (unfold-rule "repH []")
  any-call (unfold 'id)
}
one-td (unfold 'absH)