Skip to content

Commit

Permalink
Add missing showQuantity function to Reflection.AST.Show
Browse files Browse the repository at this point in the history
  • Loading branch information
jespercockx authored and andreasabel committed Jul 10, 2024
1 parent ec69137 commit 586f56a
Showing 1 changed file with 5 additions and 0 deletions.
5 changes: 5 additions & 0 deletions src/Reflection/AST/Show.agda
Original file line number Diff line number Diff line change
Expand Up @@ -24,6 +24,7 @@ open import Relation.Nullary.Decidable.Core using (yes; no)

open import Reflection.AST.Abstraction hiding (map)
open import Reflection.AST.Argument hiding (map)
open import Reflection.AST.Argument.Quantity
open import Reflection.AST.Argument.Relevance
open import Reflection.AST.Argument.Visibility
open import Reflection.AST.Argument.Modality
Expand Down Expand Up @@ -58,6 +59,10 @@ showVisibility visible = "visible"
showVisibility hidden = "hidden"
showVisibility instance′ = "instance"

showQuantity : Quantity String
showQuantity quantity-0 = "quantity-0"
showQuantity quantity-ω = "quantity-ω"

showLiteral : Literal String
showLiteral (nat x) = ℕ.show x
showLiteral (word64 x) = ℕ.show (Word64.toℕ x)
Expand Down

0 comments on commit 586f56a

Please sign in to comment.