What is the parse error referred to in this error?

user65526

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?

MrO

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

Collected from the Internet

Please contact [email protected] to delete if infringement.

edited at
0

Comments

0 comments
Login to comment

Related

What is causing a parse error in this program?

what is parse error in update panel

FInding 'server log' referred to in this postfix error

What is INSTALL_PARSE_FAILED_NO_CERTIFICATES error?

java.lang.IllegalArgumentException: error Type referred to is not an annotation type

I referred to vue.js formula, but I get an error

The code gives a parse error I can't find what the error is

What's wrong? PHP Parse error: syntax error, unexpected '}', expecting ',' or ';' in

Php error : parse error

A time.Parse Error, What am I doing wrong?

simple JSON Parse error, not sure what went wrong

Parse error: syntax error, unexpected '}'

PHP Parse error: syntax error

Parse error: syntax error, unexpected ':'

Parse error: syntax error, unexpected '=='

Haskell error "parse error on input ‘if'"

error: parse error on input `,' - Haskell

Parse error: syntax error, unexpected [

Getting parse error on input `=' error

Parse error: syntax error, unexpected '('

Parse error and no clue about the error

Error - JObject Parse Error with [] in response

ASP.NET MVC error : Object being referred to is not locked by any Client

code returns Error when reading JSON and a referred section is not Present in JSON Structure in BigQuery SQL

why does docker throw an error when I delete an image that is referred by a container?

Parse error: syntax error, unexpected T_IF, expecting ')' What should I do?

What is causing the "mount: /etc/fstab: parse error at line 16 -- ignored" error?

Java - Gson parse error

Laravel Parse error on @foreach