------------------------------------------------------------------------
-- The Agda standard library
--
-- The Pair type which calls out to Haskell via the FFI
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible #-}
module Foreign.Haskell.Pair where
open import Level using (Level; _⊔_)
open import Data.Product.Base using (_×_; _,_)
private
variable
a b : Level
A : Set a
B : Set b
------------------------------------------------------------------------
-- Definition
record Pair (A : Set a) (B : Set b) : Set (a ⊔ b) where
constructor _,_
field fst : A
snd : B
infixr 4 _,_
open Pair public
{-# FOREIGN GHC type AgdaPair l1 l2 a b = (a , b) #-}
{-# COMPILE GHC Pair = data MAlonzo.Code.Foreign.Haskell.Pair.AgdaPair ((,)) #-}
------------------------------------------------------------------------
-- Conversion
toForeign : A × B → Pair A B
toForeign (a , b) = (a , b)
{-# WARNING_ON_USAGE toForeign
"Warning: toForeign was deprecated in 2.0.
Please use Foreign.Haskell.Coerce.coerce instead."
#-}
fromForeign : Pair A B → A × B
fromForeign (a , b) = (a , b)
{-# WARNING_ON_USAGE fromForeign
"Warning: fromForeign was deprecated in 2.0.
Please use Foreign.Haskell.Coerce.coerce instead."
#-}
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4