blob: 8d024a8286f9f9d4ca4cbc708045eef1483b157b (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
|
{-# OPTIONS --without-K --safe #-}
open import Relation.Binary
module Cfe.Language.Properties
{a ℓ} (setoid : Setoid a ℓ)
where
open Setoid setoid renaming (Carrier to A)
open import Cfe.Language setoid
open import Function
------------------------------------------------------------------------
-- Properties of _≤_
≤-refl : Reflexive _≤_
≤-refl = id
≤-trans : Transitive _≤_
≤-trans A≤B B≤C = B≤C ∘ A≤B
|
