From d784b94db2556658f5d01876116df21bf1c4100b Mon Sep 17 00:00:00 2001 From: Nate Yazdani Date: Wed, 18 Sep 2019 16:32:57 -0400 Subject: [PATCH] Delete extraneous line from development --- plugin/coq/examples/Example.v | 5 ----- 1 file changed, 5 deletions(-) diff --git a/plugin/coq/examples/Example.v b/plugin/coq/examples/Example.v index b0c95328..3abc59b0 100644 --- a/plugin/coq/examples/Example.v +++ b/plugin/coq/examples/Example.v @@ -74,11 +74,6 @@ Print ltv_inv. * See Search.v for a detailed walkthrough of the output. *) -(* - * State adjunction with a slightly nicer type. - *) -Definition ltv_adjunction' : forall A x, ltv_retraction A (ltv A x) = f_equal (ltv A) (ltv_section A x) := ltv_adjunction. - (* --- Lift --- *) Lift list vector in hs_to_coq.zip as zipV_p.