From ae3264b44a7cbba53ecda762e4a7098d02fa9e43 Mon Sep 17 00:00:00 2001 From: Andreas Abel Date: Mon, 7 May 2018 17:23:38 +0200 Subject: [PATCH] Reformulated successor index case for list element. --- src/ActorMonad.lagda.tex | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/src/ActorMonad.lagda.tex b/src/ActorMonad.lagda.tex index 26a3cad..3c3fb9b 100644 --- a/src/ActorMonad.lagda.tex +++ b/src/ActorMonad.lagda.tex @@ -114,8 +114,8 @@ \AgdaDatatype{∈} is the list or set membership relation, which we model as a Peano number that tells at what position the element occurs in the list. An element that appears at the head of a list is at index \AgdaInductiveConstructor{Z}, -and an element that appears somewhere in the tail of the list is -reached by succeeding (\AgdaInductiveConstructor{S}) into the tail of the list. +and the index of an element that appears somewhere in the tail of the list is +the successor (\AgdaInductiveConstructor{S}) of its index in the tail. \AgdaCatch{Membership}{ElementIn} @@ -564,4 +564,3 @@ ⊠-of-values (x ∷ vs) = (ValueType x ∷ []) ∷ ⊠-of-values vs \end{code} % -