@@ -198,6 +198,7 @@ The first two ensure that our notions of distinct result of a program
are all preserved by the semantics. The last one intuitively states
that if $M$ has a non-erroring behavior, then $M'$ exhibits the same
behavior.
\max{Eric, see if this notion of adequacy is correct/lines up with what you prove later. If it's not just go ahead and change it to match what you are proving}
%% Here we describe the syntax and typing for the gradually-typed lambda calculus.
%% We also give the rules for syntactic type and term precision.
