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
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"
Expected Behavior
Observed Behavior