diff options
Diffstat (limited to 'tuto3/src/construction_game.ml')
| -rw-r--r-- | tuto3/src/construction_game.ml | 22 |
1 files changed, 22 insertions, 0 deletions
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 @@ -146,4 +146,26 @@ let example_classes n = 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 + 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)
\ No newline at end of file |