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