1{-# OPTIONS --no-sized-types --no-guardedness --no-subtyping #-}
2
3module Agda.Builtin.TrustMe where
4
5open import Agda.Builtin.Equality
6open import Agda.Builtin.Equality.Erase
7
8private
9  postulate
10    unsafePrimTrustMe : ∀ {a} {A : Set a} {x y : A} → x ≡ y
11
12primTrustMe : ∀ {a} {A : Set a} {x y : A} → x ≡ y
13primTrustMe = primEraseEquality unsafePrimTrustMe
14
15{-# DISPLAY primEraseEquality unsafePrimTrustMe = primTrustMe #-}
16