You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
The following is a fairly straightforward factorial implementation that recurses into an inner go function.
factorial : Nat -> Nat
factorial =
go acc n =
if n <= 1 then acc
else go (acc * n) (Nat.drop n 1)
go 1
Loading changes detected in scratch.u.
I found and typechecked these definitions in scratch.u. If you
do an `add` or `update`, here's how your codebase would
change:
⍟ These new definitions are ok to `add`:
factorial : Nat -> Nat
Now we display it:
fresh/main> display factorial
n ->
(if n <= 1 then 1
else #o5diegpfvg (1 Nat.* n) (Nat.drop n 1))
There are several weird things about this result:
It doesn't show the definition of go.
It references an unnamed term #o5diegpfvg.
The connection between the displayed and actual implementation isn't clear to me. It looks like it's mixing up n and acc. It might just be that it has been through a reduction/optimization pass, but without knowing what #o5diegpfvg looks like, it's hard to say.
Screenshots
If applicable, add screenshots to help explain your problem.
Environment (please complete the following information):
ucm --version 0.5.29
The text was updated successfully, but these errors were encountered:
Describe and demonstrate the bug
The following is a fairly straightforward factorial implementation that recurses into an inner
go
function.Now we display it:
There are several weird things about this result:
go
.#o5diegpfvg
.n
andacc
. It might just be that it has been through a reduction/optimization pass, but without knowing what#o5diegpfvg
looks like, it's hard to say.Screenshots
If applicable, add screenshots to help explain your problem.
Environment (please complete the following information):
ucm --version
0.5.29The text was updated successfully, but these errors were encountered: