mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-25 12:42:02 +03:00
20 lines
464 B
Idris
20 lines
464 B
Idris
|
module Unsafe
|
||
|
|
|
||
|
|
%default total
|
||
|
|
|
||
|
|
record Exists (p : a -> Type) where
|
||
|
|
constructor MkExists
|
||
|
|
0 x : a
|
||
|
|
prf : p x
|
||
|
|
|
||
|
|
%unsafe
|
||
|
|
lpo : (p : Nat -> Type) -> Either ((n : Nat) -> p n) (Exists $ \ n => Not (p n))
|
||
|
|
|
||
|
|
%unsafe
|
||
|
|
ext : {0 f, g : a -> b} -> ((x : a) -> f x === g x) -> f === g
|
||
|
|
|
||
|
|
example : (f : Nat -> Nat) -> Dec (f === const 0)
|
||
|
|
example f = case lpo (\ n => f n === 0) of
|
||
|
|
Left prf => Yes (ext prf)
|
||
|
|
Right (MkExists n prf) => No (\ eq => void (prf (cong ($ n) eq)))
|