From 4459f8cc7e1c3e4204b5a833e8c9e722609bf355 Mon Sep 17 00:00:00 2001
From: Yves Bertot
Date: Wed, 9 May 2018 17:44:50 +0200
Subject: checkpoint

---
 tuto3/src/construction_game.ml | 22 ++++++++++++++++++++++
 1 file changed, 22 insertions(+)

(limited to 'tuto3/src')

diff --git a/tuto3/src/construction_game.ml b/tuto3/src/construction_game.ml
index 86731c48ac..4ca59ddd36 100644
--- a/tuto3/src/construction_game.ml
+++ b/tuto3/src/construction_game.ml
@@ -127,6 +127,28 @@ let mk_nat n =
   if n <= 0 then c_O else buildup n
 
 let example_classes n =
+  let c_n = mk_nat n in
+  let n_half = mk_nat (n / 2) in
+  let c_N = c_N () in
+  let c_div = c_D () in
+  let c_even = c_E () in
+  let c_Q = c_Q () in
+  let c_R = c_R () in
+  let arg_type = EConstr.mkApp (c_even, [| c_n |]) in
+  let env = Global.env () in
+  let evd = Evd.from_env env in
+  let evd, instance = Evarutil.new_evar env evd arg_type in
+  let c_half = EConstr.mkApp (c_div, [|c_n; instance|]) in
+  let _ = Feedback.msg_notice (Termops.print_constr_env env evd c_half) in
+  let evd, the_type = Typing.type_of env evd c_half in
+  let _ = Feedback.msg_notice (Termops.print_constr_env env evd c_half) in
+  let proved_equality =
+    EConstr.mkCast(EConstr.mkApp (c_R, [| c_N; c_half |]), DEFAULTcast,
+      EConstr.mkApp (c_Q, [| c_N; c_half; n_half|])) in
+  let evd, final_type = Typing.type_of env evd proved_equality in
+  Feedback.msg_notice (Termops.print_constr_env env evd proved_equality)
+
+let example_canonical n =
   let c_n = mk_nat n in
   let n_half = mk_nat (n / 2) in
   let c_N = c_N () in
-- 
cgit v1.2.3