From 5b63add070a5dca8c8465e61a2b398215caf1af5 Mon Sep 17 00:00:00 2001
From: Philip Wadler <wadler@inf.ed.ac.uk>
Date: Fri, 14 Jul 2017 10:59:03 +0100
Subject: [PATCH] fixed symbol for numeric constants

---
 src/StlcProp.lagda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/StlcProp.lagda b/src/StlcProp.lagda
index d717c5ab..fc98c84f 100644
--- a/src/StlcProp.lagda
+++ b/src/StlcProp.lagda
@@ -815,7 +815,7 @@ data Term′ : Set where
   `_ : Id → Term′
   λ[_∶_]_ : Id → Type′ → Term′ → Term′
   _·_ : Term′ → Term′ → Term′
-  ‶_ : Data.Nat.ℕ → Term′
+  #_ : Data.Nat.ℕ → Term′
   _+_ : Term′ → Term′ → Term′
   _-_ : Term′ → Term′ → Term′
   if0_then_else_ : Term′ → Term′ → Term′ → Term′