From 4b3e4abb583dbc62018a33395d77a8384063129e Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Tue, 7 Feb 2017 15:11:54 -0500 Subject: [PATCH] Small typo fix in BasicSyntax --- BasicSyntax.v | 2 +- BasicSyntax_template.v | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) 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. *)