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 /tuto3/src | |
| parent | cb49f4c22261174f4c0a7f1a26fa795af8ed2155 (diff) | |
| parent | 4459f8cc7e1c3e4204b5a833e8c9e722609bf355 (diff) | |
This version has type inference performing proofs, using both type classes
and canonical structures
Diffstat (limited to 'tuto3/src')
| -rw-r--r-- | tuto3/src/construction_game.ml | 5 |
1 files changed, 3 insertions, 2 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) |