------------------------------------------------------------------------
-- The Agda standard library
--
-- Turn a relation into a record definition so as to remember the things
-- being related.
-- This module has a readme file: README.Data.Wrap
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
module Data.Wrap where
open import Data.Product.Nary.NonDependent
open import Function.Nary.NonDependent
open import Level using (Level)
open import Relation.Nary
private
variable
ℓ : Level
record Wrap′ {n} {ls} {A : Sets n ls} (F : A ⇉ Set ℓ) (xs : Product n A)
: Set ℓ where
constructor [_]
field
get : uncurryₙ n F xs
open Wrap′ public
Wrap : ∀ {n ls} {A : Sets n ls} → A ⇉ Set ℓ → A ⇉ Set ℓ
Wrap {n = n} F = curryₙ n (Wrap′ F)
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