我制作了一个emacs文件Prelude.agda，其中包含此页面上的信息：http://www2.tcs.ifi.lmu.de/~abel/ssft18/lec1/Prelude.agda。用C-c C-l加载后，我收到错误消息：
/Users/M/Prelude.agda:19,11-11 /Users/M/Prelude.agda:19,11::19,11: Parse error (n : ℕ) → ℕ -- To use ...
错误指向以下行：
data â„• : Set where
zero : â„•
suc : (n : ℕ) → ℕ
解析错误是什么？
网页上存在一个编码问题，您将其复制的内容粘贴到了emacs文件中，这就是为什么它不进行类型检查。
例如，应显示实体→ →，这就是为什么Agda不接受此特定定义的原因，因为它认为它应该是较早定义的某种运算符。
但是，由于编码问题遍及整个文件，因此替换此问题的特定实例将无法解决整个文件的问题。
另一个例子是â„•，应显示为ℕ。
我为您更正了该文件：
-- 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