Everything-I-Know-About-Types/bergamot-elm
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Add a text for no proofs

Browse Source
This commit is contained in:
Danila Fedorin 2023-12-29 00:07:14 -08:00
parent 98562eca2d
commit f35a8d17e8
1 changed files with 2 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
src/Main.elm
View File

@ -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 =