pl/frap
1
0
Fork 0
mirror of https://github.com/achlipala/frap.git synced 2024-11-28 07:16:20 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

Typo fixes

Browse source
This commit is contained in:
Adam Chlipala 2018-02-25 19:40:10 -05:00
parent 49b23293ca
commit 256995f1dd
2 changed files with 11 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
DataAbstraction.v
View file

@ -29,7 +29,7 @@ Set Implicit Arguments.
* implementations freedom in internal details. *) * implementations freedom in internal details. *)
Module Algebraic. Module Algebraic.
(* Here's an example of an algebraic interface or *specification* ("spec" for (* Here's an example of an algebraic interface or *specification* ("spec" for
* short). It's for purely function queues, which follow first-in-first-out * short). It's for purely functional queues, which follow first-in-first-out
* disciplines. *) * disciplines. *)
Module Type QUEUE. Module Type QUEUE.
Parameter t : Set -> Set. Parameter t : Set -> Set.
@ -619,7 +619,8 @@ Module AlgebraicWithEquivalenceRelation.
simplify. simplify.
rewrite app_nil_r in H. rewrite app_nil_r in H.
rewrite <- H in Heq1. rewrite <- H in Heq1.
rewrite rev_app_distr in Heq1. rewrite rev_app_distr in Heq1. rewrite rev_app_distr in Heq1.
rewrite rev_app_distr in Heq1.
simplify. simplify.
invert Heq1. invert Heq1.
rewrite rev_involutive. rewrite rev_involutive.
@ -1178,7 +1179,7 @@ End SET_WITH_EQUALITY.
(* Here's a generic implementation of finite sets, parameterized over an (* Here's a generic implementation of finite sets, parameterized over an
* arbitrary set with a correct equality operation. Note the use of the [with] * arbitrary set with a correct equality operation. Note the use of the [with]
* operator to *refine* the result signature [FINITE_SET]: we reveal that the * operator to *refine* the result signature [FINITE_SET]: we reveal that the
* [key] type is actually [SE.T], that is the key type from the parameter module * [key] type is actually [SE.T], that is, the key type from the parameter module
* [SE]. *) * [SE]. *)
Module ListSet(SE : SET_WITH_EQUALITY) <: FINITE_SET with Definition key := SE.t. Module ListSet(SE : SET_WITH_EQUALITY) <: FINITE_SET with Definition key := SE.t.
Definition key := SE.t. Definition key := SE.t.
@ -1749,5 +1750,5 @@ Fixpoint upto (n : nat) : list nat :=
Compute upto 10. Compute upto 10.
Compute NatDuplicateFinder.noDuplicates (upto 1000). Time Compute NatDuplicateFinder.noDuplicates (upto 1000).
Compute FasterNatDuplicateFinder.noDuplicates (upto 1000). Time Compute FasterNatDuplicateFinder.noDuplicates (upto 1000).

9
DataAbstraction_template.v
View file

@ -11,7 +11,7 @@ Set Implicit Arguments.
* implementations freedom in internal details. *) * implementations freedom in internal details. *)
Module Algebraic. Module Algebraic.
(* Here's an example of an algebraic interface or *specification* ("spec" for (* Here's an example of an algebraic interface or *specification* ("spec" for
* short). It's for purely function queues, which follow first-in-first-out * short). It's for purely functional queues, which follow first-in-first-out
* disciplines. *) * disciplines. *)
Module Type QUEUE. Module Type QUEUE.
Parameter t : Set -> Set. Parameter t : Set -> Set.
@ -463,7 +463,8 @@ Module AlgebraicWithEquivalenceRelation.
simplify. simplify.
rewrite app_nil_r in H. rewrite app_nil_r in H.
rewrite <- H in Heq1. rewrite <- H in Heq1.
rewrite rev_app_distr in Heq1. rewrite rev_app_distr in Heq1. rewrite rev_app_distr in Heq1.
rewrite rev_app_distr in Heq1.
simplify. simplify.
invert Heq1. invert Heq1.
rewrite rev_involutive. rewrite rev_involutive.
@ -1557,5 +1558,5 @@ Fixpoint upto (n : nat) : list nat :=
Compute upto 10. Compute upto 10.
Compute NatDuplicateFinder.noDuplicates (upto 1000). Time Compute NatDuplicateFinder.noDuplicates (upto 1000).
Compute FasterNatDuplicateFinder.noDuplicates (upto 1000).*) Time Compute FasterNatDuplicateFinder.noDuplicates (upto 1000).*)