Home
last modified time | relevance | path

Searched refs:defInverse (Results 1 – 3 of 3) sorted by relevance

/dports/math/hs-Agda/Agda-2.6.2/src/full/Agda/TypeChecking/
H A DInjectivity.hs274 inv <- defInverse <$> getConstInfo f
/dports/math/hs-Agda/Agda-2.6.2/src/full/Agda/TypeChecking/Monad/
H A DBase.hs2466 defInverse :: Definition -> FunctionInverse
2467 defInverse Defn{theDef = Function { funInv = inv }} = inv function
2468 defInverse Defn{theDef = Primitive{ primInv = inv }} = inv function
2469 defInverse _ = NotInjective function
/dports/math/hs-Agda/Agda-2.6.2/src/full/Agda/TypeChecking/Rules/
H A DBuiltin.hs803 inv = defInverse info