diff options
| author | Jacques Comeaux <jacquesrcomeaux@protonmail.com> | 2025-10-28 12:34:23 -0500 |
|---|---|---|
| committer | Jacques Comeaux <jacquesrcomeaux@protonmail.com> | 2025-10-28 12:34:23 -0500 |
| commit | 2cd74f160389fe2ab2b30ab628fbb9b712f06faf (patch) | |
| tree | eb81eec77cda9ed8985609f02afdb16fa86c9899 /Data/Setoid.agda | |
| parent | 8ac913160fcb3e6ec6af2b0f4cb25f45edd8212b (diff) | |
Split System into smaller modules
Diffstat (limited to 'Data/Setoid.agda')
| -rw-r--r-- | Data/Setoid.agda | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/Data/Setoid.agda b/Data/Setoid.agda new file mode 100644 index 0000000..454d276 --- /dev/null +++ b/Data/Setoid.agda @@ -0,0 +1,8 @@ +{-# OPTIONS --without-K --safe #-} + +module Data.Setoid where + +open import Relation.Binary using (Setoid) +open import Function.Construct.Setoid using () renaming (setoid to infixr 0 _⇒ₛ_) public + +open Setoid renaming (Carrier to ∣_∣) public |