mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-22 03:01:31 +03:00
f46483106f
Its purpose is to be able to formulate unversally properties which were true if function extensionality was present in the type system
12 lines
498 B
Idris
12 lines
498 B
Idris
module Control.Function.FunExt
|
|
|
|
%default total
|
|
|
|
||| This interface contains a proposition for the function extensionality.
|
|
||| It is not meant to be ever implemented.
|
|
||| It can be used to mark properties as requiring function extensionality to hold,
|
|
||| i.e. its main objective is to provide a universal way to formulate a conditional property
|
|
||| that holds only in the presence of function extensionality.
|
|
interface FunExt where
|
|
0 funExt : {0 f, g : a -> b} -> ((x : a) -> f x = g x) -> f = g
|