此错误中提到的解析错误是什么?
What is the parse error referred to in this error?
我创建了一个 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
我创建了一个 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