git.iko.soy/Idris-dev
on 385dcbf help sign in
Idris-dev/test/totality021/expected
9 lines 484 B history raw
1totality021.idr:8:1:
2Main.sLevelNotSLevel' is possibly not total due to recursive path Main.sLevelNotSLevel' --> Main.sLevelNotSLevel'
3totality021.idr:12:1:
4Main.sLevelNotSLevel is possibly not total due to: Main.sLevelNotSLevel'
5totality021.idr:18:1:Main.v is possibly not total due to: Main.sLevelNotSLevel
6totality021a.idr:9:1:
7Main.noNonEmptyPointInt is not total as there are missing cases
8totality021a.idr:12:1:
9Main.myVoid is possibly not total due to: Main.noNonEmptyPointInt