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
- + Errors (1)
`-- totality.idr line 3 col 0:
Main.foo is possibly not total due to recursive path Main.foo --> Main.foo
Observed Behavior
$ idris2 totality.idr
1/1: Building totality (totality.idr)
Welcome to Idris 2 version 0.0. Enjoy yourself!
Main> :total foo
Main.foo is not terminating due to recursive path Main.foo
The text was updated successfully, but these errors were encountered:
Steps to Reproduce
run
idris2 totality.idr
where totality.idr is:Expected Behavior
Observed Behavior
The text was updated successfully, but these errors were encountered: