'addclause' client command fails to produce a meaningful definition for helpers under 'where' blocks

[edwinb]

Issue by rgrover
Wednesday Apr 29, 2020 at 23:29 GMT
Originally opened as edwinb/Idris2-boot#341

---

Steps to Reproduce

Attempting to generate a trivial definition for the go helper function (below) fails to produce meaningful results. The behaviour can also be reproduced by running idris2 from the command line: idris2 GeneratingTrivialDefiniton.idr --client ":ac! 6 go"

module GeneratingTrivialDefiniton

recurse : (n : Nat) -> Nat
recurse n = go n 0
  where
    go : (x : Nat) -> (acc: Nat) -> Nat

Expected Behavior

module GeneratingTrivialDefiniton

recurse : (n : Nat) -> Nat
recurse n = go n 0
  where
    go : (x : Nat) -> (acc: Nat) -> Nat
    go x acc = ?go_rhs

Observed Behavior

module GeneratingTrivialDefiniton

recurse : (n : Nat) -> Nat
recurse n = go n 0
  where
    go : (x : Nat) -> (acc: Nat) -> Nat
    1143:235:go x acc = ?1143:235:go_rhs