From 25fbc53ecbb19a7489b9e0f0bf75b403cf287cea Mon Sep 17 00:00:00 2001 From: Zachary Brown Date: Wed, 29 Jan 2020 15:56:50 -0800 Subject: [PATCH] Add note about agda pragma placement --- src/plfa/part1/Naturals.lagda.md | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/src/plfa/part1/Naturals.lagda.md b/src/plfa/part1/Naturals.lagda.md index 694e3f0c..f06192ac 100644 --- a/src/plfa/part1/Naturals.lagda.md +++ b/src/plfa/part1/Naturals.lagda.md @@ -252,6 +252,20 @@ with `zero` and `suc` requires space proportional to _n_, whereas representing it as an arbitrary-precision integer in Haskell only requires space proportional to the logarithm of _n_. +Note that the data declaration must come _before_ the `BUILTIN` pragma, +as Agda will attempt to bind the given built-in to whatever name is given +in the pragma statement. As such, that name must be in scope relative to +the pragma. If you encounter a "Not in scope" error after adding the +pragma, this is likely the cause. + +Complete definition with pragma: +``` +data ℕ : Set where + zero : ℕ + suc : ℕ → ℕ +{-# BUILTIN NATURAL ℕ #-} +``` + ## Imports