From 0e74bcf948d160270dbb6810e58cfec064d94209 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Thu, 9 Feb 2017 06:58:38 -0500 Subject: [PATCH] Push the last code change through a further copy-and-paste instance --- BasicSyntax.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/BasicSyntax.v b/BasicSyntax.v index 37bc3b0..1c56c5c 100644 --- a/BasicSyntax.v +++ b/BasicSyntax.v @@ -168,7 +168,7 @@ Module ArithWithVariables. end. Compute depth ex1. - Compute size ex2. + Compute depth ex2. Theorem depth_le_size : forall e, depth e <= size e. Proof.