# HG changeset patch
# User Adam Chlipala <adamc@hcoop.net>
# Date 1225316498 14400
# Node ID eee4fd311f64e359c04adbf2c66640f338ec7a62
# Parent  e70fbfc56c464cf1a652849d32e234db71e24a01
Reflection exercise

diff -r e70fbfc56c46 -r eee4fd311f64 src/Reflection.v
--- a/src/Reflection.v	Wed Oct 29 14:39:00 2008 -0400
+++ b/src/Reflection.v	Wed Oct 29 17:41:38 2008 -0400
@@ -647,7 +647,7 @@
   %\item%#<li># Define a function [expDenote] that translates [exp]s, along with lists of rationals representing variable values, to [Q].#</li>#
   %\item%#<li># Define a recursive function [eqsDenote] over [list (exp * Q)], characterizing when all of the equations are true.#</li>#
   %\item%#<li># Fix a representation [lhs] of flattened expressions.  Where [len] is the number of variables, represent a flattened equation as [ilist Q len].  Each position of the list gives the coefficient of the corresponding variable.#</li>#
-  %\item%#<li># Write a recursive function [linearize] that takes a constant [k] and an expression [e] and optionally returns a [lhs] equivalent to [k * e].  This function returns [None] when it discovers that the input expression is not linear.  The parameter [len] of the [lhs] should be a parameter of [linearize], too.  The functions [singleton], [everywhere], and [map2] from [DepList] will probably be helpful.  It is also helpful to know that [Qplus] is the identifier for rational addition.#</li>#
+  %\item%#<li># Write a recursive function [linearize] that takes a constant [k] and an expression [e] and optionally returns a [lhs] equivalent to [k * e].  This function returns [None] when it discovers that the input expression is not linear.  The parameter [len] of [lhs] should be a parameter of [linearize], too.  The functions [singleton], [everywhere], and [map2] from [DepList] will probably be helpful.  It is also helpful to know that [Qplus] is the identifier for rational addition.#</li>#
   %\item%#<li># Write a recursive function [linearizeEqs : list (exp * Q) -> option (lhs * Q)].  This function linearizes all of the equations in the list in turn, building up the sum of the equations.  It returns [None] if the linearization of any constituent equation fails.#</li>#
   %\item%#<li># Define a denotation function for [lhs].#</li>#
   %\item%#<li># Prove that, when [exp] linearization succeeds on constant [k] and expression [e], the linearized version has the same meaning as [k * e].#</li>#