Skip to content

Commit 0f2fd19

Browse files
committed
Add _≡ᵇ_ to Reflection.Literal
1 parent e20fc59 commit 0f2fd19

File tree

1 file changed

+4
-0
lines changed

1 file changed

+4
-0
lines changed

Diff for: src/Reflection/Literal.agda

+4
Original file line numberDiff line numberDiff line change
@@ -8,6 +8,7 @@
88

99
module Reflection.Literal where
1010

11+
open import Data.Bool.Base as Bool using (Bool; true; false)
1112
import Data.Char as Char
1213
import Data.Float as Float
1314
import Data.Nat as ℕ
@@ -102,3 +103,6 @@ meta x ≟ char x₁ = no (λ ())
102103
meta x ≟ string x₁ = no (λ ())
103104
meta x ≟ name x₁ = no (λ ())
104105
meta x ≟ meta x₁ = Dec.map′ (cong meta) meta-injective (x Meta.≟ x₁)
106+
107+
_≡ᵇ_ : Literal Literal Bool
108+
l ≡ᵇ l′ = Dec.isYes (l ≟ l′)

0 commit comments

Comments
 (0)