diff options
| author | Yves Bertot | 2018-05-10 13:57:00 +0200 |
|---|---|---|
| committer | Yves Bertot | 2018-05-10 13:57:00 +0200 |
| commit | 6763c589d4097da0a58ad72adf8b201c660b8b84 (patch) | |
| tree | 9fd975f62da7145f0ee9eef8419e380346a99691 | |
| parent | cb49f4c22261174f4c0a7f1a26fa795af8ed2155 (diff) | |
| parent | 4459f8cc7e1c3e4204b5a833e8c9e722609bf355 (diff) | |
This version has type inference performing proofs, using both type classes
and canonical structures
| -rw-r--r-- | tuto3/src/construction_game.ml | 5 | ||||
| -rw-r--r-- | tuto3/theories/Data.v | 2 |
2 files changed, 3 insertions, 4 deletions
diff --git a/tuto3/src/construction_game.ml b/tuto3/src/construction_game.ml index 0a94419e83..df761b4505 100644 --- a/tuto3/src/construction_game.ml +++ b/tuto3/src/construction_game.ml @@ -173,7 +173,8 @@ let example_classes n = Feedback.msg_notice (Termops.print_constr_env env evd proved_equality) (* This function, together with definitions in Data.v, shows how to - trigger automatic proofs at the time of typechecking. + trigger automatic proofs at the time of typechecking, based on + canonical structures. n is a number for which we want to find the half (and a proof that this half is indeed the half) @@ -213,4 +214,4 @@ let example_canonical n = let evd, the_statement = Typing.type_of env evd the_prf in Feedback.msg_notice (Termops.print_constr_env env evd the_prf ++ str " has type " ++ - Termops.print_constr_env env evd the_statement)
\ No newline at end of file + Termops.print_constr_env env evd the_statement) diff --git a/tuto3/theories/Data.v b/tuto3/theories/Data.v index c288d5d452..b2afffed68 100644 --- a/tuto3/theories/Data.v +++ b/tuto3/theories/Data.v @@ -23,7 +23,6 @@ Canonical Structure can_ev_default n d (Pd : 2 * n = d) : S_ev n := Canonical Structure can_ev0 : S_ev 0 := Build_S_ev 0 0 (@eq_refl _ 0). - Lemma can_ev_rec n : forall (s : S_ev n), S_ev (S n). Proof. intros s; exists (S (S (double_of _ s))). @@ -42,4 +41,3 @@ Check (C _ _ _ eq_refl : cmp 6 _). Check (C _ _ _ eq_refl : cmp 7 _). *) - |