What is the parse error referred to in this error?

Question

I made an emacs file Prelude.agda containing the information on this page: http://www2.tcs.ifi.lmu.de/~abel/ssft18/lec1/Prelude.agda. After loading with C-c C-l I receive the error:

/Users/M/Prelude.agda:19,11-11 /Users/M/Prelude.agda:19,11::19,11: Parse error (n : ℕ) → ℕ -- To use ...

The error points to the following line:

data ℕ : Set where zero : ℕ suc : (n : ℕ) → ℕ

What is the parse error?

Answer 1

There is an encoding problem on the web page whose content you copy pasted in your emacs file, which is why it does not typecheck.

For example, the entity → should be displayed → which is why Agda does not accept this specific definition because it thinks it should be some kind of operator defined earlier.

However, since the encoding problem is all over the file, replacing this specific instance of the problem would not solve it for the whole file.

Another example is â„• that should appear as ℕ.

---

I corrected the file for you:

-- 8th Summer School on Formal Techniques

-- Menlo College, Atherton, California, US
--
-- 21-25 May 2018
--
-- Lecture 1: Introduction to Agda
--
-- File 1: The Curry-Howard Isomorphism

{-# OPTIONS --allow-unsolved-metas #-}

module Prelude where

-- Natural numbers as our first example of
-- an inductive data type.

data ℕ : Set where
  zero : ℕ
  suc  : (n : ℕ) → ℕ

-- To use decimal notation for numerals, like
-- 2 instead of (suc (suc zero)), connect it
-- to the built-in natural numbers.

{-# BUILTIN NATURAL ℕ #-}

-- Lists are a parameterized inductive data type.

data List (A : Set) : Set where
  []  : List A
  _∷_ : (x : A) (xs : List A) → List A   -- \ : :

infixr 6 _∷_

-- C-c C-l   load

-- Disjoint sum type.

data _⊎_ (S T : Set) : Set where  -- \uplus
  inl : S → S ⊎ T
  inr : T → S ⊎ T

infixr 4 _⊎_

-- The empty sum is the type with 0 alternatives,
-- which is the empty type.
-- By the Curry-Howard-Isomorphism,
-- which views a proposition as the set/type of its proofs,
-- it is also the absurd proposition.

data False : Set where

⊥-elim : False → {A : Set} → A
⊥-elim () {A}

-- C-c C-SPC give
-- C-c C-, show hypotheses and goal
-- C-c C-. show hypotheses and infers type

-- Tuple types

-- The generic record type with two fields
-- where the type of the second depends on the value of the first
-- is called Sigma-type (or dependent sum), in analogy to
--
--   ∑ ℕ A =  ∑   A(n) = A(0) + A(1) + ...
--           n ∈ ℕ

record ∑ (A : Set) (B : A → Set) : Set where  -- \GS  \Sigma
  constructor _,_
  field  fst : A
         snd : B fst
open ∑

-- module ∑ {A : Set} {B : A → Set} (p : ∑ A B) where
--   fst : A
--   fst = case p of (a , b) -> a
--   snd : B fst
--   snd = case p of (a , b) -> b

infixr 5 _,_

-- The non-dependent version is the ordinary Cartesian product.

_×_ : (S T : Set) → Set
S × T = ∑ S λ _ → T

infixr 5 _×_

-- The record type with no fields has exactly one inhabitant
-- namely the empty tuple record{}
-- By Curry-Howard, it corresponds to Truth, as
-- no evidence is needed to construct this proposition.

record True : Set where

test : True
test = _

-- C-c C-=  show constraints
-- C-c C-r  refine
-- C-c C-s  solve
-- C-c C-SPC give
-- C-c C-a   auto

-- Example: distributivity  A × (B ⊎ C) → (A × B) ⊎ (A × C)

dist : ∀ {A B C : Set} → A × (B ⊎ C) → (A × B) ⊎ (A × C)
dist (a , inl b) = inl (a , b)
dist (a , inr c) = inr (a , c)

dist' : ∀ {A B : Set} → A × (B ⊎ A) → (A × B) ⊎ (A × A)
dist' (a , inl b) = inl (a , b)
dist' (a , inr c) = inr (c , c)

-- Relations

-- Type-theoretically, the type of relations over (A×A) is
--
--   A × A → Prop
--
-- which is
--
--   A × A → Set
--
-- by the Curry-Howard-Isomorphism
-- and
--
--   A → A → Set
--
-- by currying.

Rel : (A : Set) → Set₁
Rel A = A → A → Set

-- Less-or-equal on natural numbers

_≤_ : Rel ℕ
zero  ≤ y     = True
suc x ≤ zero  = False
suc x ≤ suc y = x ≤ y

-- C-c C-l load
-- C-c C-c case split
-- C-c C-, show goal and assumptions
-- C-c C-. show goal and assumptions and current term
-- C-c C-SPC give