Allow single constructor types in proof search

2024-11-11 14:57:30 +03:00 · 2015-08-12 15:28:37 +01:00 · 2015-08-12 15:28:37 +01:00 · 6e7c036b13
commit 6e7c036b13
parent 65f49450e3
1 changed files with 2 additions and 1 deletions
--- a/src/Idris/ProofSearch.hs
+++ b/src/Idris/ProofSearch.hs
@ -203,7 +203,8 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot psnames hi
                      case lookupCtxtExact n (idris_datatypes ist) of
                          Just t -> do
                             let others = hints ++ con_names t ++ autohints
-                             when (not fromProver) -- in interactive mode,
+                             when (not fromProver && length (con_names t) > 1)
+                                   -- in interactive mode,
                                   -- don't just guess (fine for 'auto',
                                   -- since that's part of the point...)
                                   $ checkConstructor ist others