added a hint when the user obviously just forgot a colon after the lemma's name
authorblanchet
Tue Dec 07 11:56:01 2010 +0100 (2010-12-07 ago)
changeset 41048d5ebe94248ad
parent 41047 9f1d3fcef1ca
child 41049 0edd245892ed
added a hint when the user obviously just forgot a colon after the lemma's name
src/HOL/Tools/Nitpick/nitpick.ML
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Tue Dec 07 11:56:01 2010 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Tue Dec 07 11:56:01 2010 +0100
     1.3 @@ -179,6 +179,10 @@
     1.4  
     1.5  fun none_true assigns = forall (not_equal (SOME true) o snd) assigns
     1.6  
     1.7 +fun has_lonely_bool_var (@{const Pure.conjunction}
     1.8 +                         $ (@{const Trueprop} $ Free _) $ _) = true
     1.9 +  | has_lonely_bool_var _ = false
    1.10 +
    1.11  val syntactic_sorts =
    1.12    @{sort "{default,zero,one,plus,minus,uminus,times,inverse,abs,sgn,ord,equal}"} @
    1.13    @{sort number}
    1.14 @@ -661,7 +665,9 @@
    1.15                      \section for details (\"isabelle doc nitpick\")."
    1.16              else
    1.17                ();
    1.18 -            if has_syntactic_sorts orig_t then
    1.19 +            if has_lonely_bool_var orig_t then
    1.20 +              print "Hint: Maybe you forgot a colon after the lemma's name?"
    1.21 +            else if has_syntactic_sorts orig_t then
    1.22                print "Hint: Maybe you forgot a type constraint?"
    1.23              else
    1.24                ();