------------------------------------------------------------------------ -- The Agda standard library -- -- Strictness combinators ------------------------------------------------------------------------ {-# OPTIONS --without-K --safe #-} module Strict where open import Level open import Agda.Builtin.Equality open import Agda.Builtin.Strict renaming ( primForce to force ; primForceLemma to force-≡) public -- Derived combinators module _ { ℓ′ : Level} {A : Set } {B : Set ℓ′} where force′ : A (A B) B force′ = force force′-≡ : (a : A) (f : A B) force′ a f f a force′-≡ = force-≡ seq : A B B seq a b = force a _ b) seq-≡ : (a : A) (b : B) seq a b b seq-≡ a b = force-≡ a _ b)