a different fix to issue #42, this time making explicit the TermInst …

…on the term generated from the case pattern of induction

proof_checker.py

@@ -1251,7 +1251,12 @@ def check_proof_of(proof, formula, env):
 
             trm = pattern_to_term(indcase.pattern)
             new_trm = type_check_term(trm, typ, body_env, None, [])
-            pre_goal = instantiate(loc, formula, new_trm)
+            # The following type synthesis step is because the term may get
+            # inserted into a synthesis context, and if its
+            # a TermInst, it needs to be marked as not-inferred so that it
+            # gets printed. -Jeremy
+            newer_trm = type_synth_term(new_trm, body_env, None, [])
+            pre_goal = instantiate(loc, formula, newer_trm)
             goal = check_formula(pre_goal, body_env)
 
             for ((x,frm1),frm2) in zip(indcase.induction_hypotheses, induction_hypotheses):
@@ -1739,8 +1744,6 @@ def type_check_term_inst(loc, subject, tyargs, inferred, synth):
       inst_param_types = [t.substitute(sub) for t in param_types]
       inst_return_type = return_type.substitute(sub)
       retty = FunctionType(loc2, [], inst_param_types, inst_return_type)
-      if synth and len(typarams) > 0:
-          inferred = False
     case GenericUnknownInst(loc2, union_type):
       retty = TypeInst(loc2, union_type, tyargs)
       if synth:
@@ -1763,8 +1766,6 @@ def type_check_term_inst_var(loc, subject_var, tyargs, inferred, env, synth):
           inst_param_types = [t.substitute(sub) for t in param_types]
           inst_return_type = return_type.substitute(sub)
           retty = FunctionType(loc3, [], inst_param_types, inst_return_type)
-          if synth and len(typarams) > 0:
-              inferred = False
         case GenericUnknownInst(loc3, union_type):
           retty = TypeInst(loc3, union_type, tyargs)
           if synth:

test/should-error/have_remove_marks.pf.err

@@ -1,6 +1,6 @@
 ./test/should-error/have_remove_marks.pf:11.3-11.4: incomplete proof
 Goal:
-	@length<Nat>([x]) = 1
+	length([x]) = 1
 Advice:
 	To prove this equality, one of these statements might help:
 		definition

test/should-error/sum_foldr.pf.err

@@ -1,9 +1,9 @@
 ./test/should-error/sum_foldr.pf:14.5-14.33: 
 suffices to prove:
-	0 = @foldr<Nat,Nat>([], 0, operator +)
+	0 = foldr(@[]<Nat>, 0, operator +)
 ./test/should-error/sum_foldr.pf:15.5-15.6: incomplete proof
 Goal:
-	0 = @foldr<Nat,Nat>([], 0, operator +)
+	0 = foldr(@[]<Nat>, 0, operator +)
 Advice:
 	To prove this equality, one of these statements might help:
 		definition