From b36fb6410178ab11594ff22ae1c077a351cb7b58 Mon Sep 17 00:00:00 2001
From: Raphael Cauderlier
Date: Fri, 1 Dec 2017 17:33:58 +0100
Subject: [PATCH] Typos
---
manual.org | 22 +++++++++++-----------
meta/tac.dk | 2 +-
2 files changed, 12 insertions(+), 12 deletions(-)
diff --git a/manual.org b/manual.org
index 5b0f39f..80e4a2d 100644
--- a/manual.org
+++ b/manual.org
@@ -130,7 +130,7 @@ by logical connectives and quantifiers.
An atom is a predicate symbol applied to terms respecting the arity of
the predicate symbol. Predicate symbols and their arities are defined
similarly to function symbols. A predicate symbol is a Dedukti term of
-type =fol.predicate=. An artity is is associated to each predicate
+type =fol.predicate=. An artity is associated to each predicate
symbol by the function
- =fol.pred_arity : fol.predicate -> fol.types=
@@ -220,7 +220,7 @@ definable so Deduction Modulo first-order theories can be defined.
** Equality
We treat equality as a first-order theory defined in the file
-[[./fol/eq.dl][fol/eq.dk]]. Equality is a family of predicate symbols parameterized by
+[[./fol/eq.dk][fol/eq.dk]]. Equality is a family of predicate symbols parameterized by
a sort:
- =eq.Eq : fol.type -> fol.predicate=
@@ -251,14 +251,14 @@ facts:
The Dedukti theory presented in [[* Multi-sorted first-order logic in Dedukti][the previous section]] is sound in the
following sense:
- Convergence: The rewrite system that defines it is both confluent
- and terminating
+ and terminating.
- Subject-reduction: Typing is preserved by reduction according to
- this rewrite-system
+ this rewrite-system.
- Decidability of type-checking: The type-checking problem for terms
in this Dedukti theory is decidable and the Dedukti type checker is
a decision procedure for it.
- Consistency: a closed term of type =fol.proof fol.false= can only be
- obtained by encoding an inconsistent first-order theory
+ obtained by encoding an inconsistent first-order theory.
Thanks to these good properties, a term of type =fol.proof A= can be
considered as a proof witnessing the truth of the proposition =A=. We
@@ -277,10 +277,10 @@ The first bad system is a dependently-typed tactic language. It is
very similar to the typed tactic languages of Lean and [[http://plv.mpi-sws.org/mtac/][Mtac]] but it is
simpler for the following reasons:
- It deals with first-order logic instead of the full calculus of
- inductive constructions
+ inductive constructions.
- In Dedukti it is not necessary to encode pattern matching and
recursion directly in the tactic language because the user can
- already use rewriting for these tasks
+ already use rewriting for these tasks.
- We have chosen to keep a shallow encoding of terms and formulae so
some features such as testing whether a term is a variable are
omitted.
@@ -296,7 +296,7 @@ to handle failure and backtracking.
- =tac.bind : A : fol.prop -> B : fol.prop -> tac.tactic A -> (fol.proof A -> tac.tactic B) -> tac.tactic B=
If =A= is a formula, =tac.tactic A= is the Dedukti type of the tactics
-attempting to prove =A=. It forms a monad whise return and bind
+attempting to prove =A=. It forms a monad whose return and bind
operations are =tac.ret= and =tac.bind= respectively.
When a tactic successfully proves a formula, we can extract a proof of the formula using the partial function =tac.run=:
@@ -359,7 +359,7 @@ The certificate language is described in file [[./meta/cert.dk][meta/cert.dk]].
** Contexts and certificate evaluation
-=certificate= is the Dedukti type of certificates. Contrary to
+=cert.certificate= is the Dedukti type of certificates. Contrary to
tactics, the type of a certificate does not indicate which formula it
is supposed to prove and the same certificate can in fact prove
several formulae.
@@ -546,8 +546,8 @@ The certificate =cert.apply A B a c= proves =B a= if =c= proves
*** Reasoning on the goal
-The following certificates each prove the current goal if it has a
-particular shape:
+The following certificates are used to reason on the current goal,
+each proves the current goal if it has a particular shape:
- =cert.trivial : cert.certificate=
- =cert.split : cert.certificate -> cert.certificate -> cert.certificate=
- =cert.left : cert.certificate -> cert.certificate=
diff --git a/meta/tac.dk b/meta/tac.dk
index aee1e01..d52881d 100644
--- a/meta/tac.dk
+++ b/meta/tac.dk
@@ -7,7 +7,7 @@
(setq-local dedukti-compile-options '("-nc" "-e" "-nl" "-I" "../fol"))
;)
-(; This is a Meta Dedukti port Mtac with the following simpifications:
+(; This is a Meta Dedukti port of Mtac with the following simpifications:
- works on first-order logic instead of CIC
This implies a bit of duplication between terms and proofs.
- nu and abs are replaced by the less powerful but simpler to implement intro
--
2.24.1