From 54e43d2c5f8c2f095bda4ff19ad56153369f2630 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Fri, 24 Jun 2016 14:09:48 -0400 Subject: incorporate `Program Definition` match statement handling advice from @mattam82 --- folkwisdom.md | 14 +++++++++----- 1 file changed, 9 insertions(+), 5 deletions(-) (limited to 'folkwisdom.md') diff --git a/folkwisdom.md b/folkwisdom.md index e1c52351c..d87174115 100644 --- a/folkwisdom.md +++ b/folkwisdom.md @@ -110,11 +110,15 @@ involves nontrivial considerations of its own). The most reliable way to make a value of a sigma type is to start the `Definition` in proof mode (ending the first line with a dot like `Definition zero : point.`) and then do `refine (exist _ value _); abstract -(tacticThatProvesInvariant)`. Some of the time, `Program Definition` will do the -same thing without explicit proof mode (as the Edwards curve spec) but it tends -to over-eagerly rewrite `if` and `match` statements (as in the Weierstrass curve -spec). Neatness of the value that is defined takes priority over neatness of the -code that performs the definition. +(tacticThatProvesInvariant)`. Another way of doing this is to first do +`Obligation Tactic := tacticThatProvesInvariant.` and then `Program Definition +zero : point := exist _ value _.` which will call the tactic to fill in the +holes that implicit argument inference does not fill. By default, `Program +Definition` rewrites all match statements using the convoy pattern, and this can +clutter definitions quite badly. Neatness of resulting definitions takes +priority over neatness of source code. To prevent `Program Definition` to +rewriting a match statement, specify an explicit return clause: `match x return +_ with ... end.` ## Equivalence -- cgit v1.2.3