A RetroSearch Logo

Home - News ( United States | United Kingdom | Italy | Germany ) - Football scores

Search Query:

Showing content from https://agda.github.io/agda-stdlib/master/Data.Unit.Instances.html below:

Data.Unit.Instances

Data.Unit.Instances
------------------------------------------------------------------------
-- The Agda standard library
--
-- Instances for the unit type
------------------------------------------------------------------------

{-# OPTIONS --cubical-compatible --safe #-}

module Data.Unit.Instances where

open import Data.Unit.Properties using (_≟_; ≡-isDecTotalOrder)
open import Relation.Binary.PropositionalEquality.Properties
  using (isDecEquivalence)

instance
  ⊤-≡-isDecEquivalence = isDecEquivalence _≟_
  ⊤-≤-isDecTotalOrder = ≡-isDecTotalOrder

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