Idris2/tests/idris2/failing/failing003/FailingTotality.idr

module FailingTotality

%default total

failing "x is not covering."

  x : Bool -> Nat
  x True = 0


failing "x is not total, possibly not terminating due to recursive
         path FailingTotality.x"

  x : Bool
  x = x

failing "D is not total, not strictly positive"

  data D : Type where
    Lam : (D -> D) -> D
[ fix #2402 ] Check totality before exiting failing block 2022-04-08 00:57:08 +03:00			`module FailingTotality`

			`%default total`

			`failing "x is not covering."`

			`x : Bool -> Nat`
			`x True = 0`


			`failing "x is not total, possibly not terminating due to recursive`
[ termination ] faithful implementation of size-change graph termination analysis - call sequences in termination errors now carry location information - new error message (`BadPath`) for late-starting loops - [ fix ] transitive closure of size-change graphs no longer ignores function arguments - update existing tests accordingly 2023-02-06 20:37:41 +03:00			`path FailingTotality.x"`
[ fix #2402 ] Check totality before exiting failing block 2022-04-08 00:57:08 +03:00
			`x : Bool`
			`x = x`

			`failing "D is not total, not strictly positive"`

			`data D : Type where`
			`Lam : (D -> D) -> D`