From 403ab6cac4f8c81e033e271518f484578e3ece79 Mon Sep 17 00:00:00 2001 From: cuibuwei Date: Mon, 2 Dec 2024 20:40:15 +0800 Subject: [PATCH] chore: remove redundant words in comment Signed-off-by: cuibuwei --- doc/papers/system-f-in-agda/paper.lagda | 2 +- doc/plutus-core-spec/flat-serialisation.tex | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/doc/papers/system-f-in-agda/paper.lagda b/doc/papers/system-f-in-agda/paper.lagda index f6172b8f18a..3b216f6a26b 100644 --- a/doc/papers/system-f-in-agda/paper.lagda +++ b/doc/papers/system-f-in-agda/paper.lagda @@ -2618,7 +2618,7 @@ with conversion presented in section \ref{sec:intrinsically-typed}. We define two special cases of \AgdaFunction{subst} which allow us to substitute the types of variables or terms by propositionally equal types. While it is the case that types are now represented uniquely we -still want or need to to prove that two types are equal, especially in +still want or need to prove that two types are equal, especially in the presence of (Agda) variables, cf., while the natural number 7 has a unique representation in Agda we still might want to prove that for any natural numbers \AgdaBound{m} and \AgdaBound{n}, \AgdaBound{m} diff --git a/doc/plutus-core-spec/flat-serialisation.tex b/doc/plutus-core-spec/flat-serialisation.tex index a323c2f0c48..6461877dd35 100644 --- a/doc/plutus-core-spec/flat-serialisation.tex +++ b/doc/plutus-core-spec/flat-serialisation.tex @@ -85,7 +85,7 @@ \subsection{Padding} then $\pad$ still adds an extra byte of padding; $\pad$ is used both for internal alignment (for example, to make sure that the contents of a bytestring are aligned on byte boundaries) and at the end of a complete encoding of a -Plutus Core program to to make the length a multiple of 8 bits. +Plutus Core program to make the length a multiple of 8 bits. Symbolically, $$ \pad(s) = s \cdot \pp{k} \quad \text{if $\length(s) = 8n+k$ with $n,k \in \N$ and $0 \leq k \leq 7$}