| Copyright | (c) Galois Inc 2014-2021 |
|---|---|
| Safe Haskell | Unsafe |
| Language | Haskell2010 |
Data.Parameterized.Axiom
Description
An unsafe module that provides functionality for constructing equality proofs that GHC cannot prove on its own.
Synopsis
- unsafeAxiom :: forall {k} (a :: k) (b :: k). a :~: b
- unsafeHeteroAxiom :: forall {k1} {k2} (a :: k1) (b :: k2). a :~~: b
Documentation
unsafeAxiom :: forall {k} (a :: k) (b :: k). a :~: b Source #
Assert a proof of equality between two types. This is unsafe if used improperly, so use this with caution!
unsafeHeteroAxiom :: forall {k1} {k2} (a :: k1) (b :: k2). a :~~: b Source #
Assert a proof of heterogeneous equality between two types. This is unsafe if used improperly, so use this with caution!