Idris2Doc : Control.Function.FunExt

Control.Function.FunExt

Definitions

interfaceFunExt : 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 : {0b : a->Type} -> ((x : a) ->fx=gx) ->f=g
funExt : FunExt=> {0b : a->Type} -> ((x : a) ->fx=gx) ->f=g
Totality: total
Visibility: public export