mirror of
https://github.com/luau-lang/luau.git
synced 2024-11-16 06:45:44 +08:00
10 lines
247 B
Agda
10 lines
247 B
Agda
|
module Properties.Remember where
|
||
|
|
|
||
|
|
open import Agda.Builtin.Equality using (_≡_; refl)
|
||
|
|
|
||
|
|
data Remember {A : Set} (a : A) : Set where
|
||
|
|
_,_ : ∀ b → (a ≡ b) → Remember(a)
|
||
|
|
|
||
|
|
remember : ∀ {A} (a : A) → Remember(a)
|
||
|
|
remember a = (a , refl)
|