mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-17 00:10:31 +03:00
53 lines
1.2 KiB
Plaintext
53 lines
1.2 KiB
Plaintext
1/1: Building Issue1771-1 (Issue1771-1.idr)
|
|
Error: Fix is not total, not strictly positive
|
|
|
|
Issue1771-1:3:1--4:29
|
|
3 | data Fix : (Type -> Type) -> Type where
|
|
4 | MkFix : f (Fix f) -> Fix f
|
|
|
|
Error: MkFix is not total, not strictly positive
|
|
|
|
Issue1771-1:4:3--4:8
|
|
1 | %default total
|
|
2 |
|
|
3 | data Fix : (Type -> Type) -> Type where
|
|
4 | MkFix : f (Fix f) -> Fix f
|
|
^^^^^
|
|
|
|
Error: yesF is not total, possibly not terminating due to call to Main.MkFix
|
|
|
|
Issue1771-1:9:1--9:18
|
|
5 |
|
|
6 | F : Type
|
|
7 | F = Fix Not
|
|
8 |
|
|
9 | yesF : Not F -> F
|
|
^^^^^^^^^^^^^^^^^
|
|
|
|
1/1: Building Issue1771-2 (Issue1771-2.idr)
|
|
Error: F is not total, not strictly positive
|
|
|
|
Issue1771-2:3:1--4:58
|
|
3 | data F : Type where
|
|
4 | MkFix : ((0 g : Type -> Type) -> g === Not -> g F) -> F
|
|
|
|
Error: MkFix is not total, not strictly positive
|
|
|
|
Issue1771-2:4:3--4:8
|
|
1 | %default total
|
|
2 |
|
|
3 | data F : Type where
|
|
4 | MkFix : ((0 g : Type -> Type) -> g === Not -> g F) -> F
|
|
^^^^^
|
|
|
|
Error: yesF is not total, possibly not terminating due to call to Main.MkFix
|
|
|
|
Issue1771-2:6:1--6:18
|
|
2 |
|
|
3 | data F : Type where
|
|
4 | MkFix : ((0 g : Type -> Type) -> g === Not -> g F) -> F
|
|
5 |
|
|
6 | yesF : Not F -> F
|
|
^^^^^^^^^^^^^^^^^
|
|
|