Delete extraneous line from development

uwplse · Sep 18, 2019 · d784b94 · d784b94
1 parent 31cdb1c
commit d784b94
Showing 1 changed file with 0 additions and 5 deletions.
diff --git 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.