diff options
| author | FabianWolff <fabi.wolff@arcor.de> | 2020-09-01 05:20:57 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-08-31 20:20:57 -0700 |
| commit | fa05eb5599e2ac0b2d4c1e0e943fee6353b52430 (patch) | |
| tree | f3c9cbb78e7e80657e0a0ebcd5f438842d05a854 /proofs/signatures/th_lira.plf | |
| parent | 09b3b246ad0328a163b0e3825531ccf82ea4013d (diff) | |
Fix spelling errors (#4977)
Signed-off-by: Fabian Wolff <fabi.wolff@arcor.de>
Diffstat (limited to 'proofs/signatures/th_lira.plf')
| -rw-r--r-- | proofs/signatures/th_lira.plf | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/proofs/signatures/th_lira.plf b/proofs/signatures/th_lira.plf index af326bf27..e3f6df112 100644 --- a/proofs/signatures/th_lira.plf +++ b/proofs/signatures/th_lira.plf @@ -128,7 +128,7 @@ (default (fail (term Int))) )) -; This function negates linear interger terms---sums of terms of the form +; This function negates linear integer terms---sums of terms of the form ; recognized by `negate_linear_monomial_int_term`. (program negate_linear_int_term ((t (term Int))) (term Int) (match t @@ -339,7 +339,7 @@ ; the statement that `a` satisfies `b` for all inputs (declare bounded_aff (! a aff (! b bound formula))) -; Sum of two bounds (the bound satisfied by the sum of two functions satifying +; Sum of two bounds (the bound satisfied by the sum of two functions satisfying ; the input bounds) (program bound_add ((b bound) (b2 bound)) bound (match b |