0 | module BeTTI.FunExt
 1 |
 2 | import System
 3 | import System.File
 4 |
 5 | %default total
 6 |
 7 | public export 0
 8 | FunExt : (f,g : a -> b) -> Type
 9 | FunExt f g = (x : a) -> f x = g x
10 |
11 | export 0
12 | funext : (f,g : a -> b) -> FunExt f g -> f = g
13 | funext f g prf = believe_me $ unsafePerformIO (do
14 |      _ <- fPutStrLn stderr "Trying to execute function extensionality"
15 |      exitWith {a = f = g} $ ExitFailure 1)
16 |