mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-19 09:12:34 +03:00
140 lines
3.1 KiB
Plaintext
140 lines
3.1 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: argh is not total, possibly not terminating due to function Main.MkFix being reachable via Main.yesF -> Main.MkFix
|
|
|
|
Issue1771-1:15:1--15:12
|
|
11 |
|
|
12 | notF : Not F
|
|
13 | notF (MkFix f) = f (yesF f)
|
|
14 |
|
|
15 | argh : Void
|
|
^^^^^^^^^^^
|
|
|
|
Error: notF is not total, possibly not terminating due to call to Main.yesF
|
|
|
|
Issue1771-1:12:1--12:13
|
|
08 |
|
|
09 | yesF : Not F -> F
|
|
10 | yesF nf = MkFix nf
|
|
11 |
|
|
12 | notF : Not 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: argh is not total, possibly not terminating due to function Main.MkFix being reachable via Main.yesF -> Main.MkFix
|
|
|
|
Issue1771-2:14:1--14:12
|
|
10 | notF (MkFix f) =
|
|
11 | let g = f Not Refl in
|
|
12 | g (yesF g)
|
|
13 |
|
|
14 | argh : Void
|
|
^^^^^^^^^^^
|
|
|
|
Error: notF is not total, possibly not terminating due to call to Main.yesF
|
|
|
|
Issue1771-2:9:1--9:13
|
|
5 |
|
|
6 | yesF : Not F -> F
|
|
7 | yesF nf = MkFix (\ g, Refl => nf)
|
|
8 |
|
|
9 | notF : Not 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
|
|
^^^^^^^^^^^^^^^^^
|
|
|
|
1/1: Building Issue1771-3 (Issue1771-3.idr)
|
|
Error: F is not total, not strictly positive
|
|
|
|
Issue1771-3:9:1--10:26
|
|
09 | data F : Type where
|
|
10 | MkF : Wrap (Not F) -> F
|
|
|
|
Error: MkF is not total, not strictly positive
|
|
|
|
Issue1771-3:10:3--10:6
|
|
06 | unwrap : Wrap a -> a
|
|
07 | unwrap (MkWrap v) = v
|
|
08 |
|
|
09 | data F : Type where
|
|
10 | MkF : Wrap (Not F) -> F
|
|
^^^
|
|
|
|
Error: argh is not total, possibly not terminating due to function Main.MkF being reachable via Main.yesF -> Main.MkF
|
|
|
|
Issue1771-3:18:1--18:12
|
|
14 |
|
|
15 | notF : Not F
|
|
16 | notF (MkF f) = unwrap f (yesF $ unwrap f)
|
|
17 |
|
|
18 | argh : Void
|
|
^^^^^^^^^^^
|
|
|
|
Error: notF is not total, possibly not terminating due to calls to Main.F, Main.yesF
|
|
|
|
Issue1771-3:15:1--15:13
|
|
11 |
|
|
12 | yesF : Not F -> F
|
|
13 | yesF = MkF . MkWrap
|
|
14 |
|
|
15 | notF : Not F
|
|
^^^^^^^^^^^^
|
|
|
|
Error: yesF is not total, possibly not terminating due to call to Main.MkF
|
|
|
|
Issue1771-3:12:1--12:18
|
|
08 |
|
|
09 | data F : Type where
|
|
10 | MkF : Wrap (Not F) -> F
|
|
11 |
|
|
12 | yesF : Not F -> F
|
|
^^^^^^^^^^^^^^^^^
|
|
|