From 85aca1dda24c5933d803b195570514df219e51d8 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Wed, 30 Oct 2019 15:24:32 +0100 Subject: Return of Refine Instance as an attribute. We can now do `#[refine] Instance : Bla := bli.` to enter proof mode with `bli` as a starting refinement. If `bli` is enough to define the instance we still enter proof mode, keeping things nicely predictable for the stm. --- .../10996-refine-instance-returns.rst | 4 ++++ doc/sphinx/addendum/type-classes.rst | 19 ++++++++++++++++--- 2 files changed, 20 insertions(+), 3 deletions(-) create mode 100644 doc/changelog/02-specification-language/10996-refine-instance-returns.rst (limited to 'doc') diff --git a/doc/changelog/02-specification-language/10996-refine-instance-returns.rst b/doc/changelog/02-specification-language/10996-refine-instance-returns.rst new file mode 100644 index 0000000000..cd1a692f54 --- /dev/null +++ b/doc/changelog/02-specification-language/10996-refine-instance-returns.rst @@ -0,0 +1,4 @@ +- Added ``#[refine]`` attribute for :cmd:`Instance`, a more + predictable version of the old ``Refine Instance Mode`` which + unconditionally opens a proof (`#10996 + `_, by Gaëtan Gilbert). diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst index 1bbf988505..57a2254100 100644 --- a/doc/sphinx/addendum/type-classes.rst +++ b/doc/sphinx/addendum/type-classes.rst @@ -47,9 +47,22 @@ Leibniz equality on some type. An example implementation is: | tt, tt => eq_refl tt end }. -Using :cmd:`Program Instance`, if one does not give all the members in -the Instance declaration, Coq generates obligations for the remaining -fields, e.g.: +Using the attribute ``refine``, if the term is not sufficient to +finish the definition (e.g. due to a missing field or non-inferable +hole) it must be finished in proof mode. If it is sufficient a trivial +proof mode with no open goals is started. + +.. coqtop:: in + + #[refine] Instance unit_EqDec' : EqDec unit := { eqb x y := true }. + Proof. intros [] [];reflexivity. Defined. + +Note that if you finish the proof with :cmd:`Qed` the entire instance +will be opaque, including the fields given in the initial term. + +Alternatively, in :flag:`Program Mode` if one does not give all the +members in the Instance declaration, Coq generates obligations for the +remaining fields, e.g.: .. coqtop:: in -- cgit v1.2.3