From f35a8d17e8e8b23641ffd2ab9e9a7e1dd2370e54 Mon Sep 17 00:00:00 2001
From: Danila Fedorin <danila.fedorin@gmail.com>
Date: Fri, 29 Dec 2023 00:07:14 -0800
Subject: [PATCH] Add a text for no proofs

---
 src/Main.elm | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/Main.elm b/src/Main.elm
index 58fd050..0468319 100644
--- a/src/Main.elm
+++ b/src/Main.elm
@@ -221,7 +221,8 @@ viewProofTree : ResultMode -> Term Metavariable -> (RuleEnv, RuleEnv) -> Result
 viewProofTree resultMode query (prog, renderProg) =
     case single prog (prove query |> Bergamot.Rules.andThen reifyProofTree) of
         Just proofTree -> renderProofTree resultMode proofTree renderProg
-        Nothing -> Ok <| Html.div [ class "bergamot-no-proofs" ] []
+        Nothing -> Ok <| Html.div [ class "bergamot-no-proofs" ]
+            [ Html.text "No applicable rules to prove input" ]
 
 view : Model -> Html Msg
 view m =