2022-02-10 07:14:29 +08:00
|
|
|
module Luau.Var where
|
|
|
|
|
|
|
|
|
|
open import Agda.Builtin.Bool using (true; false)
|
|
|
|
|
open import Agda.Builtin.Equality using (_≡_)
|
|
|
|
|
open import Agda.Builtin.String using (String; primStringEquality)
|
|
|
|
|
open import Agda.Builtin.TrustMe using (primTrustMe)
|
2022-03-03 06:02:51 +08:00
|
|
|
open import Properties.Dec using (Dec; yes; no)
|
|
|
|
|
open import Properties.Equality using (_≢_)
|
2022-02-10 07:14:29 +08:00
|
|
|
|
|
|
|
|
Var : Set
|
|
|
|
|
Var = String
|
|
|
|
|
|
|
|
|
|
_≡ⱽ_ : (a b : Var) → Dec (a ≡ b)
|
|
|
|
|
a ≡ⱽ b with primStringEquality a b
|
2022-03-03 06:02:51 +08:00
|
|
|
a ≡ⱽ b | false = no p where postulate p : (a ≢ b)
|
2022-02-10 07:14:29 +08:00
|
|
|
a ≡ⱽ b | true = yes primTrustMe
|
