Skip to content

Commit b773b73

Browse files
jespercockxandreasabel
authored andcommitted
Export missing IsDecEquivalence instance for Quantity from Reflection.AST.Instances
1 parent d3c5037 commit b773b73

File tree

1 file changed

+2
-0
lines changed

1 file changed

+2
-0
lines changed

src/Reflection/AST/Instances.agda

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -17,6 +17,7 @@ import Reflection.AST.Abstraction as Abstraction
1717
import Reflection.AST.Argument as Argument
1818
import Reflection.AST.Argument.Visibility as Visibility
1919
import Reflection.AST.Argument.Relevance as Relevance
20+
import Reflection.AST.Argument.Quantity as Quantity
2021
import Reflection.AST.Argument.Information as Information
2122
import Reflection.AST.Pattern as Pattern
2223
import Reflection.AST.Term as Term
@@ -37,6 +38,7 @@ instance
3738
Meta-≡-isDecEquivalence = isDecEquivalence Meta._≟_
3839
Visibility-≡-isDecEquivalence = isDecEquivalence Visibility._≟_
3940
Relevance-≡-isDecEquivalence = isDecEquivalence Relevance._≟_
41+
Quantity-≡-isDecEquivalence = isDecEquivalence Quantity._≟_
4042
ArgInfo-≡-isDecEquivalence = isDecEquivalence Information._≟_
4143
Pattern-≡-isDecEquivalence = isDecEquivalence Pattern._≟_
4244
Clause-≡-isDecEquivalence = isDecEquivalence Term._≟-Clause_

0 commit comments

Comments
 (0)