/usr/share/agda-stdlib/Relation/Binary/EqReasoning.agda is in agda-stdlib 0.6-2.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 | ------------------------------------------------------------------------
-- The Agda standard library
--
-- Convenient syntax for equational reasoning
------------------------------------------------------------------------
-- Example use:
-- n*0≡0 : ∀ n → n * 0 ≡ 0
-- n*0≡0 zero = refl
-- n*0≡0 (suc n) =
-- begin
-- suc n * 0
-- ≈⟨ refl ⟩
-- n * 0 + 0
-- ≈⟨ ... ⟩
-- n * 0
-- ≈⟨ n*0≡0 n ⟩
-- 0
-- ∎
-- Note that some modules contain generalised versions of specific
-- instantiations of this module. For instance, the module ≡-Reasoning
-- in Relation.Binary.PropositionalEquality is recommended for
-- equational reasoning when the underlying equality is
-- Relation.Binary.PropositionalEquality._≡_.
open import Relation.Binary
module Relation.Binary.EqReasoning {s₁ s₂} (S : Setoid s₁ s₂) where
open Setoid S
import Relation.Binary.PreorderReasoning as PreR
open PreR preorder public
renaming ( _∼⟨_⟩_ to _≈⟨_⟩_
; _≈⟨_⟩_ to _≡⟨_⟩_
)
|