------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties for Conats
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --sized-types #-}
module Codata.Sized.Conat.Properties where
open import Codata.Sized.Conat
open import Codata.Sized.Conat.Bisimilarity using (_⊢_≈_; refl; zero; suc)
open import Codata.Sized.Thunk using (Thunk; Thunk^R; force)
open import Data.Nat.Base using (ℕ; zero; suc)
open import Function.Base using (_∋_)
open import Relation.Binary.Definitions using (Decidable)
open import Relation.Nullary.Decidable.Core using (yes; no; map′)
open import Relation.Nullary.Negation.Core using (¬_)
open import Size using (Size)
private
variable
i : Size
0∸m≈0 : ∀ m → i ⊢ zero ∸ m ≈ zero
0∸m≈0 zero = refl
0∸m≈0 (suc m) = 0∸m≈0 m
sℕ≤s⁻¹ : ∀ {m n} → suc m ℕ≤ suc n → m ℕ≤ n .force
sℕ≤s⁻¹ (sℕ≤s p) = p
infix 4 _ℕ≤?_
_ℕ≤?_ : Decidable _ℕ≤_
zero ℕ≤? n = yes zℕ≤n
suc m ℕ≤? zero = no (λ ())
suc m ℕ≤? suc n = map′ sℕ≤s sℕ≤s⁻¹ (m ℕ≤? n .force)
0ℕ+-identity : ∀ {n} → i ⊢ 0 ℕ+ n ≈ n
0ℕ+-identity = refl
+ℕ0-identity : ∀ {n} → i ⊢ n +ℕ 0 ≈ n
+ℕ0-identity {n = zero} = zero
+ℕ0-identity {n = suc n} = suc λ where .force → +ℕ0-identity
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