Control.Function.FunExt(source)

Definitions

interface FunExt : Type

  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.

Methods:

funExt : {0 b : a -> Type} -> ((x : a) -> f x = g x) -> f = g

funExt : FunExt => {0 b : a -> Type} -> ((x : a) -> f x = g x) -> f = g

Totality: total
Visibility: public export

funExt0 : FunExt => {0 b : a -> Type} -> ((x : a) -> f x = g x) -> f = g

Totality: total
Visibility: export

funExt1 : FunExt => {0 b : a -> Type} -> ((x : a) -> f x = g x) -> f = g

Totality: total
Visibility: export