diff --git a/BasicSyntax.v b/BasicSyntax.v index 1948495..37bc3b0 100644 --- a/BasicSyntax.v +++ b/BasicSyntax.v @@ -52,7 +52,7 @@ Module ArithWithConstants. end. Compute depth ex1. - Compute size ex2. + Compute depth ex2. (* Our first proof! * Size is an upper bound on depth. *) diff --git a/BasicSyntax_template.v b/BasicSyntax_template.v index b52c393..1d15b02 100644 --- a/BasicSyntax_template.v +++ b/BasicSyntax_template.v @@ -32,7 +32,7 @@ Fixpoint depth (e : arith) : nat := end. Compute depth ex1. -Compute size ex2. +Compute depth ex2. (* Our first proof! * Size is an upper bound on depth. *)