------------------------------------------------------------------------
-- The Agda standard library
--
-- An equality postulate which evaluates
------------------------------------------------------------------------

{-# OPTIONS --with-K #-}

module Relation.Binary.PropositionalEquality.TrustMe where

open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)

open import Agda.Builtin.TrustMe

-- trustMe {x = x} {y = y} evaluates to refl if x and y are
-- definitionally equal.

trustMe : ∀ {a} {A : Set a} {x y : A} → x ≡ y
trustMe = primTrustMe

-- "Erases" a proof. The original proof is not inspected. The
-- resulting proof reduces to refl if the two sides are definitionally
-- equal. Note that checking for definitional equality can be slow.

erase : ∀ {a} {A : Set a} {x y : A} → x ≡ y → x ≡ y
erase _ = trustMe

-- A "postulate with a reduction": postulate[ a ↦ b ] a evaluates to b,
-- while postulate[ a ↦ b ] a′ gets stuck if a′ is not definitionally
-- equal to a. This can be used to define a postulate of type (x : A) → B x
-- by only specifying the behaviour at B t for some t : A. Introduced in
--
--   Alan Jeffrey, Univalence via Agda's primTrustMe again
--   23 January 2015
--   https://lists.chalmers.se/pipermail/agda/2015/007418.html

postulate[_↦_] : ∀ {a b} {A : Set a}{B : A → Set b} →
                  (t : A) → B t → (x : A) → B x
postulate[ a ↦ b ] a′ with trustMe {x = a} {a′}
postulate[ a ↦ b ] .a | refl = b