From a03579e8f3c1d3dfcfe08c3c81a1795b45ede513 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@Inria.fr>
Date: Wed, 2 Dec 2020 15:08:59 +0100
Subject: [PATCH] typos (thanks K. Maillard)

---
 examples/tutorial_elpi_lang.v | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/examples/tutorial_elpi_lang.v b/examples/tutorial_elpi_lang.v
index 409348961..809129fcd 100644
--- a/examples/tutorial_elpi_lang.v
+++ b/examples/tutorial_elpi_lang.v
@@ -217,7 +217,7 @@ Elpi Query lp:{{
 
 (**
    An even harder query is the following one where we ask for two distinct
-   indivisuals to have the same age.
+   individuals to have the same age.
 *)
 
 Elpi Query lp:{{
@@ -234,7 +234,7 @@ Elpi Query lp:{{
    forces the last choice that was made to be reconsidered,
    so "Q" becomes "bob".
 
-   Look at the outout of the following instrumented code:
+   Look at the output of the following instrumented code:
 *)
 
 Elpi Query lp:{{
@@ -251,7 +251,7 @@ Elpi Query lp:{{
    In general clauses can have premises, that is conditions necessary in
    order to make the predicate hold.
 
-   Here we add to our program a clase that defiens what "older P Q" means
+   Here we add to our program a clase that defines what "older P Q" means
    in terms of the "age" of "P" and "Q". Note that ">" is a built-in predicate.
 *)
 Elpi Accumulate lp:{{
@@ -320,7 +320,7 @@ Elpi Query lp:{{
    symbol or a clause variable (that required the convention of
    using capitals for variables).
 
-   Functions build using λ-abstraction can be applied
+   Functions built using λ-abstraction can be applied
    to arguments and honor the usual β-reduction rule
    (the argument is substituted for the bound variable).
 
@@ -963,7 +963,7 @@ Fail Elpi Query lp:{{ sigma Y\ pi x\ Y = x }}.
       𝚪 ⊦ λx.f : A → B
 
    on paper, the x being bound can only occur in f (not in 𝚪 or B for example).
-   Reamrk that in the premise x is still bound, this time not by a λ but by the
+   Remark that in the premise x is still bound, this time not by a λ but by the
    context 𝚪, x : A. In λProlog the context is the set of hypothetical clauses
    and pi-quantified variables and is implicitly handled by the runtime of the
    programming language.