We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
showQuantity
1 parent b773b73 commit a055438Copy full SHA for a055438
src/Reflection/AST/Show.agda
@@ -24,6 +24,7 @@ open import Relation.Nullary.Decidable.Core using (yes; no)
24
25
open import Reflection.AST.Abstraction hiding (map)
26
open import Reflection.AST.Argument hiding (map)
27
+open import Reflection.AST.Argument.Quantity
28
open import Reflection.AST.Argument.Relevance
29
open import Reflection.AST.Argument.Visibility
30
open import Reflection.AST.Argument.Modality
@@ -58,6 +59,10 @@ showVisibility visible = "visible"
58
59
showVisibility hidden = "hidden"
60
showVisibility instance′ = "instance"
61
62
+showQuantity : Quantity → String
63
+showQuantity quantity-0 = "quantity-0"
64
+showQuantity quantity-ω = "quantity-ω"
65
+
66
showLiteral : Literal → String
67
showLiteral (nat x) = ℕ.show x
68
showLiteral (word64 x) = ℕ.show (Word64.toℕ x)
0 commit comments