Compare commits
No commits in common. "4deb7bc556f9ba3c2bb82ae668fdf19e69c6c036" and "efe0efbee7c55a14251c074e48d26c9896b68c15" have entirely different histories.
4deb7bc556
...
efe0efbee7
2
elm.json
2
elm.json
@ -9,10 +9,10 @@
|
||||
"elm/browser": "1.0.2",
|
||||
"elm/core": "1.0.5",
|
||||
"elm/html": "1.0.0",
|
||||
"elm/json": "1.1.3",
|
||||
"elm/parser": "1.1.0"
|
||||
},
|
||||
"indirect": {
|
||||
"elm/json": "1.1.3",
|
||||
"elm/time": "1.0.0",
|
||||
"elm/url": "1.0.0",
|
||||
"elm/virtual-dom": "1.0.3"
|
||||
|
||||
60
index.html
60
index.html
@ -1,60 +0,0 @@
|
||||
<!DOCTYPE HTML>
|
||||
<html>
|
||||
<head>
|
||||
<meta charset="UTF-8">
|
||||
<meta name="viewport" content="width=device-width, initial-scale=1" />
|
||||
<title>Main</title>
|
||||
<script type="module" src="https://unpkg.com/@navsnpm/katex-expression/dist/katex-expression/katex-expression.esm.js"></script>
|
||||
<script nomodule="" src="https://unpkg.com/@navsnpm/katex-expression/dist/katex-expression/katex-expression.js"></script>
|
||||
<style>body { padding: 0; margin: 0; }</style>
|
||||
<style>
|
||||
textarea {
|
||||
display: block;
|
||||
width: 100%;
|
||||
height: 10em;
|
||||
resize: none;
|
||||
}
|
||||
|
||||
input[type="text"] {
|
||||
width: 100%;
|
||||
}
|
||||
|
||||
.rule-list {
|
||||
display: flex;
|
||||
flex-direction: row;
|
||||
flex-wrap: wrap;
|
||||
justify-content: center;
|
||||
}
|
||||
|
||||
.rule-list katex-expression {
|
||||
margin-left: .5em;
|
||||
margin-right: .5em;
|
||||
flex-grow: 1;
|
||||
flex-basis: 0;
|
||||
}
|
||||
|
||||
.elm-root {
|
||||
max-width: 800px;
|
||||
margin: auto;
|
||||
padding: 1em;
|
||||
border: 1px solid #c3c3c3;
|
||||
border-radius: 0.5em;
|
||||
margin-top: 1em;
|
||||
}
|
||||
|
||||
.elm-root h2 {
|
||||
margin-bottom: 0.5em;
|
||||
}
|
||||
</style>
|
||||
</head>
|
||||
|
||||
<body>
|
||||
<div id="elm"></div>
|
||||
<script src="index.js"></script>
|
||||
<script>
|
||||
var app = Elm.Main.init({
|
||||
node: document.getElementById('elm')
|
||||
});
|
||||
</script>
|
||||
</body>
|
||||
</html>
|
||||
@ -1,35 +0,0 @@
|
||||
module Bergamot.Latex exposing (..)
|
||||
|
||||
import Bergamot.Syntax exposing (..)
|
||||
import Bergamot.Rules exposing (..)
|
||||
|
||||
termToLatex : (a -> String) -> Term a -> String
|
||||
termToLatex f t =
|
||||
case t of
|
||||
Call "type" [t1, t2] -> termToLatex f t1 ++ " : " ++ termToLatex f t2
|
||||
Call "intlit" [t1] -> termToLatex f t1
|
||||
Call "strlit" [t1] -> termToLatex f t1
|
||||
Call "tpair" [t1, t2] -> termToLatex f t1 ++ "\\times" ++ termToLatex f t2
|
||||
Call "plus" [t1, t2] -> termToLatex f t1 ++ " + " ++ termToLatex f t2
|
||||
Call "pair" [t1, t2] -> "(" ++ termToLatex f t1 ++ ", " ++ termToLatex f t2 ++ ")"
|
||||
Call s [] -> "\\text{" ++ s ++ "}"
|
||||
Call s ts -> "\\text{" ++ s ++ "}(" ++ String.join "," (List.map (termToLatex f) ts) ++ ")"
|
||||
Var x -> f x
|
||||
IntLit i -> String.fromInt i
|
||||
StringLit s -> "\"" ++ s ++ "\""
|
||||
|
||||
metavariableToLatex : Metavariable -> String
|
||||
metavariableToLatex (MkMetavariable s) =
|
||||
let
|
||||
noQuestion = String.dropLeft 1 s
|
||||
in
|
||||
if String.startsWith "tau" noQuestion then "\\" ++ noQuestion else noQuestion
|
||||
|
||||
ruleToLatex : Rule -> String
|
||||
ruleToLatex r = "\\cfrac{" ++ String.join "\\quad " (List.map (termToLatex metavariableToLatex) r.premises) ++ "}{" ++ termToLatex metavariableToLatex r.conclusion ++ "}\\ \\texttt{" ++ r.name ++ "}"
|
||||
|
||||
unificationVarToLatex : UnificationVar -> String
|
||||
unificationVarToLatex (MkUnificationVar s) = s
|
||||
|
||||
proofTreeToLatex : ProofTree -> String
|
||||
proofTreeToLatex (MkProofTree node) = "\\cfrac{" ++ String.join "\\quad \\quad " (List.map proofTreeToLatex node.premises) ++ "}{" ++ termToLatex unificationVarToLatex node.conclusion ++ "}\\ \\texttt{" ++ node.name ++ "}"
|
||||
@ -1,6 +1,6 @@
|
||||
module Bergamot.Parser exposing (..)
|
||||
|
||||
import Bergamot.Syntax exposing (Term(..), Metavariable(..))
|
||||
import Bergamot.Syntax exposing (Term(..), Metavariable)
|
||||
import Bergamot.Rules exposing (Rule, RuleEnv)
|
||||
|
||||
import Parser exposing (Parser, Trailing(..), (|.), (|=))
|
||||
@ -16,14 +16,12 @@ name = Parser.variable
|
||||
, reserved = Set.empty
|
||||
}
|
||||
|
||||
variable : Parser Metavariable
|
||||
variable =
|
||||
Parser.succeed MkMetavariable
|
||||
|= Parser.variable
|
||||
{ start = \c -> c == '?'
|
||||
, inner = \c -> Char.isAlphaNum c || c == '_'
|
||||
, reserved = Set.empty
|
||||
}
|
||||
variable : Parser String
|
||||
variable = Parser.variable
|
||||
{ start = \c -> c == '?'
|
||||
, inner = \c -> Char.isAlphaNum c || c == '_'
|
||||
, reserved = Set.empty
|
||||
}
|
||||
|
||||
term : Parser (Term Metavariable)
|
||||
term = Parser.lazy (\() -> Parser.oneOf
|
||||
|
||||
@ -1,6 +1,6 @@
|
||||
module Bergamot.Rules exposing (..)
|
||||
|
||||
import Bergamot.Syntax exposing (Term, Metavariable, UnificationVar, unify, emptyUnificationState, instantiate, instantiateList, emptyInstantiationState, resetVars, InstantiationState, UnificationState, reify)
|
||||
import Bergamot.Syntax exposing (Term, Metavariable, UnificationVar, unify, emptyUnificationState, instantiate, instantiateList, emptyInstantiationState, resetVars, InstantiationState, UnificationState)
|
||||
import Bergamot.Search as Search exposing (Search)
|
||||
|
||||
import Debug
|
||||
@ -33,26 +33,11 @@ andThen f p env ps =
|
||||
p env ps
|
||||
|> Search.andThen (\(a, psp) -> (f a) env psp)
|
||||
|
||||
join : Prover (Prover a) -> Prover a
|
||||
join p = andThen (\x -> x) p
|
||||
|
||||
apply : Prover a -> Prover (a -> b) -> Prover b
|
||||
apply pa pf = pf |> andThen (\f -> map f pa)
|
||||
|
||||
map : (a -> b) -> Prover a -> Prover b
|
||||
map f p env ps =
|
||||
p env ps
|
||||
|> Search.map (Tuple.mapFirst f)
|
||||
|
||||
mapM : (a -> Prover b) -> List a -> Prover (List b)
|
||||
mapM f l =
|
||||
case l of
|
||||
x :: xs ->
|
||||
pure (::)
|
||||
|> apply (f x)
|
||||
|> apply (mapM f xs)
|
||||
[] -> pure []
|
||||
|
||||
interleave : Prover a -> Prover a -> Prover a
|
||||
interleave p1 p2 env ps =
|
||||
Search.interleave (p1 env ps) (p2 env ps)
|
||||
@ -66,56 +51,34 @@ fail env ps = Search.fail
|
||||
getEnv : Prover RuleEnv
|
||||
getEnv env ps = Search.pure (env, ps)
|
||||
|
||||
getUnificationState : Prover UnificationState
|
||||
getUnificationState env ps = Search.pure (ps.unificationState, ps)
|
||||
|
||||
liftInstantiation : (a -> InstantiationState -> (b, InstantiationState)) -> a -> Prover b
|
||||
liftInstantiation f a env ps =
|
||||
let
|
||||
(b, is) = f a ps.instantiationState
|
||||
in
|
||||
Search.pure (b, { ps | instantiationState = is })
|
||||
|
||||
liftUnification : (a -> a -> UnificationState -> Maybe (a, UnificationState)) -> a -> a -> Prover a
|
||||
liftUnification f a1 a2 env ps =
|
||||
case f a1 a2 ps.unificationState of
|
||||
Just (a, us) -> Search.pure (a, { ps | unificationState = us })
|
||||
Nothing -> Search.fail
|
||||
|
||||
withVars : Prover a -> Prover a
|
||||
withVars p env ps =
|
||||
p env ps
|
||||
|> Search.map (Tuple.mapSecond (\psp -> { psp | instantiationState = resetVars psp.instantiationState }))
|
||||
|
||||
|
||||
reifyProofTree : ProofTree -> Prover ProofTree
|
||||
reifyProofTree (MkProofTree node) =
|
||||
pure (\t trees -> MkProofTree { node | conclusion = t, premises = trees })
|
||||
|> apply (map (reify node.conclusion) getUnificationState)
|
||||
|> apply (mapM reifyProofTree node.premises)
|
||||
|
||||
rule : Term UnificationVar -> Rule -> Prover ProofTree
|
||||
rule t r =
|
||||
withVars (pure Tuple.pair
|
||||
|> apply (liftInstantiation instantiate r.conclusion)
|
||||
|> apply (liftInstantiation instantiateList r.premises))
|
||||
|> andThen (\(conc, prems) ->
|
||||
pure (\tp trees -> MkProofTree { name = r.name, conclusion = tp, premises = trees })
|
||||
|> apply (liftUnification unify t conc)
|
||||
|> apply (provePremises prems))
|
||||
rule t r env ps =
|
||||
let
|
||||
(conc, is) = instantiate r.conclusion ps.instantiationState
|
||||
(prems, isp) = instantiateList r.premises is
|
||||
in
|
||||
case unify t conc ps.unificationState of
|
||||
Nothing -> Search.fail
|
||||
Just (tp, usp) ->
|
||||
let
|
||||
psp = { ps | instantiationState = resetVars isp
|
||||
, unificationState = usp }
|
||||
in
|
||||
provePremises prems env psp
|
||||
|> Search.map (Tuple.mapFirst (\trees -> MkProofTree { name = r.name, conclusion = tp, premises = trees }))
|
||||
|
||||
provePremises : List (Term UnificationVar) -> Prover (List ProofTree)
|
||||
provePremises = mapM proveTerm
|
||||
provePremises l =
|
||||
case l of
|
||||
t :: ts ->
|
||||
prove t
|
||||
|> andThen (\tree -> map (\trees -> tree :: trees) (provePremises ts))
|
||||
[] -> pure []
|
||||
|
||||
proveTerm : Term UnificationVar -> Prover ProofTree
|
||||
proveTerm t =
|
||||
prove : Term UnificationVar -> Prover ProofTree
|
||||
prove t =
|
||||
getEnv
|
||||
|> andThen (\env -> List.foldl (\r -> interleave (rule t r)) fail env.rules)
|
||||
|
||||
prove : Term Metavariable -> Prover ProofTree
|
||||
prove mt =
|
||||
liftInstantiation instantiate mt
|
||||
|> andThen proveTerm
|
||||
|> andThen (List.foldl (\r -> interleave (rule t r)) fail << .rules)
|
||||
|
||||
single : RuleEnv -> Prover a -> Maybe a
|
||||
single env p =
|
||||
|
||||
@ -12,11 +12,11 @@ map f s () =
|
||||
Empty -> Empty
|
||||
Found a sp -> Found (f a) (map f sp)
|
||||
|
||||
apply : Search a -> Search (a -> b) -> Search b
|
||||
apply sa sf () =
|
||||
apply : Search (a -> b) -> Search a -> Search b
|
||||
apply sf sa () =
|
||||
case sf () of
|
||||
Empty -> Empty
|
||||
Found f sfp -> interleave (map f sa) (apply sa sfp) ()
|
||||
Found f sfp -> interleave (map f sa) (apply sfp sa) ()
|
||||
|
||||
andThen : (a -> Search b) -> Search a -> Search b
|
||||
andThen f sa () =
|
||||
|
||||
@ -1,5 +1,5 @@
|
||||
module Bergamot.Syntax exposing
|
||||
( Term(..), Metavariable(..), UnificationVar(..)
|
||||
( Term(..), Metavariable, UnificationVar
|
||||
, instantiate, instantiateList, InstantiationState, emptyInstantiationState, resetVars
|
||||
, unify, unifyList, UnificationState, emptyUnificationState
|
||||
, reify
|
||||
@ -12,14 +12,8 @@ import Tuple
|
||||
import Debug
|
||||
|
||||
type alias Name = String
|
||||
type Metavariable = MkMetavariable String
|
||||
type UnificationVar = MkUnificationVar String
|
||||
|
||||
unMetavariable : Metavariable -> String
|
||||
unMetavariable (MkMetavariable s) = s
|
||||
|
||||
unUnificationVar : UnificationVar -> String
|
||||
unUnificationVar (MkUnificationVar s) = s
|
||||
type alias Metavariable = String
|
||||
type alias UnificationVar = String
|
||||
|
||||
type Term a
|
||||
= IntLit Int
|
||||
@ -29,7 +23,7 @@ type Term a
|
||||
|
||||
type alias InstantiationState =
|
||||
{ counter : Int
|
||||
, vars : Dict String UnificationVar
|
||||
, vars : Dict Metavariable UnificationVar
|
||||
}
|
||||
|
||||
emptyInstantiationState = { counter = 0, vars = Dict.empty }
|
||||
@ -39,15 +33,12 @@ resetVars is = { is | vars = Dict.empty }
|
||||
|
||||
metavariable : Metavariable -> InstantiationState -> (UnificationVar, InstantiationState)
|
||||
metavariable mv is =
|
||||
case Dict.get (unMetavariable mv) is.vars of
|
||||
case Dict.get mv is.vars of
|
||||
Just v -> (v, is)
|
||||
Nothing ->
|
||||
let
|
||||
v = MkUnificationVar ("var" ++ (String.fromInt is.counter))
|
||||
isp =
|
||||
{ counter = is.counter + 1
|
||||
, vars = Dict.insert (unMetavariable mv) v is.vars
|
||||
}
|
||||
v = "var" ++ (String.fromInt is.counter)
|
||||
isp = { counter = is.counter + 1, vars = Dict.insert mv v is.vars }
|
||||
in (v, isp)
|
||||
|
||||
instantiateList : List (Term Metavariable) -> InstantiationState -> (List (Term UnificationVar), InstantiationState)
|
||||
@ -67,58 +58,51 @@ instantiate mt is =
|
||||
Var mv -> Tuple.mapFirst Var (metavariable mv is)
|
||||
|
||||
type alias UnificationInfo =
|
||||
{ equivalence : Set String
|
||||
{ equivalence : Set UnificationVar
|
||||
, term : Maybe (Term UnificationVar)
|
||||
}
|
||||
|
||||
type alias UnificationState = Dict String UnificationInfo
|
||||
type alias UnificationState = Dict UnificationVar UnificationInfo
|
||||
|
||||
emptyUnificationState = Dict.empty
|
||||
|
||||
reconcile : Set String -> Maybe (Term UnificationVar) -> UnificationState -> UnificationState
|
||||
reconcile : Set UnificationVar -> Maybe (Term UnificationVar) -> UnificationState -> UnificationState
|
||||
reconcile eq mt us =
|
||||
let newValue = { equivalence = eq, term = mt }
|
||||
in Set.foldl (\v -> Dict.insert v newValue) us eq
|
||||
|
||||
merge : UnificationVar -> UnificationVar -> UnificationState -> Maybe UnificationState
|
||||
merge v1 v2 us =
|
||||
let
|
||||
v1s = unUnificationVar v1
|
||||
v2s = unUnificationVar v2
|
||||
in
|
||||
case (Dict.get v1s us, Dict.get v2s us) of
|
||||
(Just ui1, Just ui2) ->
|
||||
let
|
||||
newEq = Set.union ui1.equivalence ui2.equivalence
|
||||
in
|
||||
case (ui1.term, ui2.term) of
|
||||
(Just t1, Just t2) ->
|
||||
unify t1 t2 us
|
||||
|> Maybe.map (\(t, usp) -> reconcile newEq (Just t) usp)
|
||||
(Just t1, Nothing) ->
|
||||
Just (reconcile newEq (Just t1) us)
|
||||
(Nothing, Just t2) ->
|
||||
Just (reconcile newEq (Just t2) us)
|
||||
(Nothing, Nothing) ->
|
||||
Just (reconcile newEq Nothing us)
|
||||
(Just ui1, Nothing) -> Just (reconcile (Set.insert v2s ui1.equivalence) ui1.term us)
|
||||
(Nothing, Just ui2) -> Just (reconcile (Set.insert v1s ui2.equivalence) ui2.term us)
|
||||
(Nothing, Nothing) -> Just (reconcile (Set.fromList [v1s,v2s]) Nothing us)
|
||||
case (Dict.get v1 us, Dict.get v2 us) of
|
||||
(Just ui1, Just ui2) ->
|
||||
let
|
||||
newEq = Set.union ui1.equivalence ui2.equivalence
|
||||
in
|
||||
case (ui1.term, ui2.term) of
|
||||
(Just t1, Just t2) ->
|
||||
unify t1 t2 us
|
||||
|> Maybe.map (\(t, usp) -> reconcile newEq (Just t) usp)
|
||||
(Just t1, Nothing) ->
|
||||
Just (reconcile newEq (Just t1) us)
|
||||
(Nothing, Just t2) ->
|
||||
Just (reconcile newEq (Just t2) us)
|
||||
(Nothing, Nothing) ->
|
||||
Just (reconcile newEq Nothing us)
|
||||
(Just ui1, Nothing) -> Just (reconcile (Set.insert v2 ui1.equivalence) ui1.term us)
|
||||
(Nothing, Just ui2) -> Just (reconcile (Set.insert v1 ui2.equivalence) ui2.term us)
|
||||
(Nothing, Nothing) -> Just (reconcile (Set.fromList [v1,v2]) Nothing us)
|
||||
|
||||
set : UnificationVar -> Term UnificationVar -> UnificationState -> Maybe (Term UnificationVar, UnificationState)
|
||||
set v t us =
|
||||
let
|
||||
vs = unUnificationVar v
|
||||
in
|
||||
case Dict.get vs us of
|
||||
Just ui ->
|
||||
case ui.term of
|
||||
Just tp ->
|
||||
unify t tp us
|
||||
|> Maybe.map (\(tpp, usp) -> (tpp, reconcile ui.equivalence (Just tpp) usp))
|
||||
Nothing ->
|
||||
Just (t, reconcile ui.equivalence (Just t) us)
|
||||
Nothing -> Just (t, Dict.insert vs { equivalence = Set.singleton vs, term = Just t } us)
|
||||
case Dict.get v us of
|
||||
Just ui ->
|
||||
case ui.term of
|
||||
Just tp ->
|
||||
unify t tp us
|
||||
|> Maybe.map (\(tpp, usp) -> (tpp, reconcile ui.equivalence (Just tpp) usp))
|
||||
Nothing ->
|
||||
Just (t, reconcile ui.equivalence (Just t) us)
|
||||
Nothing -> Just (t, Dict.insert v { equivalence = Set.singleton v, term = Just t } us)
|
||||
|
||||
unifyList : List (Term UnificationVar) -> List (Term UnificationVar) -> UnificationState -> Maybe (List (Term UnificationVar), UnificationState)
|
||||
unifyList l1 l2 us =
|
||||
@ -152,7 +136,7 @@ reify t us =
|
||||
StringLit s -> StringLit s
|
||||
Call n ts -> Call n (List.map (\tp -> reify tp us) ts)
|
||||
Var v ->
|
||||
case Dict.get (unUnificationVar v) us of
|
||||
case Dict.get v us of
|
||||
Just ui ->
|
||||
case ui.term of
|
||||
Just tp -> reify tp us
|
||||
|
||||
66
src/Main.elm
66
src/Main.elm
@ -3,70 +3,32 @@ module Main exposing (main)
|
||||
import Browser
|
||||
import Html exposing (Html)
|
||||
import Html.Events exposing (onInput)
|
||||
import Html.Attributes exposing (type_, class)
|
||||
import Bergamot.Syntax exposing (..)
|
||||
import Bergamot.Search exposing (..)
|
||||
import Bergamot.Rules exposing (..)
|
||||
import Bergamot.Parser exposing (..)
|
||||
import Bergamot.Latex exposing (..)
|
||||
import Json.Encode
|
||||
import Maybe
|
||||
import Tuple
|
||||
import Debug
|
||||
|
||||
type alias Model =
|
||||
{ program : String
|
||||
, query : String
|
||||
}
|
||||
type alias Model = { program : String }
|
||||
type alias Flags = ()
|
||||
type Msg
|
||||
= SetProgram String
|
||||
| SetQuery String
|
||||
|
||||
init : Flags -> (Model, Cmd Msg)
|
||||
init () = ({ program = "", query = "" }, Cmd.none)
|
||||
|
||||
viewSection : String -> Html Msg -> Html Msg
|
||||
viewSection name content =
|
||||
Html.div [] [ Html.h2 [] [ Html.text name ], content ]
|
||||
|
||||
viewRule : Rule -> Html Msg
|
||||
viewRule = latex << ruleToLatex
|
||||
|
||||
viewRules : String -> Html Msg
|
||||
viewRules progs = viewSection "Rendered Rules" <|
|
||||
Html.div [ class "rule-list" ] <|
|
||||
case run program progs of
|
||||
Just prog -> List.map viewRule prog.rules
|
||||
Nothing -> []
|
||||
|
||||
tryProve : String -> String -> Maybe ProofTree
|
||||
tryProve progs querys =
|
||||
case (run program progs, run term querys) of
|
||||
(Just prog, Just query) -> single prog (prove query |> Bergamot.Rules.andThen reifyProofTree)
|
||||
_ -> Nothing
|
||||
|
||||
viewProofTree : String -> String -> Html Msg
|
||||
viewProofTree progs querys = viewSection "Proof Tree" <|
|
||||
Html.div [ class "proof-tree" ] <|
|
||||
case tryProve progs querys of
|
||||
Just tree -> [ latex (proofTreeToLatex tree) ]
|
||||
Nothing -> []
|
||||
|
||||
init () = ({ program = "" }, Cmd.none)
|
||||
|
||||
view : Model -> Html Msg
|
||||
view m = Html.div [ class "elm-root" ]
|
||||
[ viewSection "Rules" <| Html.textarea [ onInput SetProgram ] []
|
||||
, viewSection "Query" <| Html.input [ type_ "text", onInput SetQuery ] []
|
||||
, viewRules m.program
|
||||
, viewProofTree m.program m.query
|
||||
view m = Html.div []
|
||||
[ Html.textarea [ onInput SetProgram ] []
|
||||
, Html.p [] [ Html.text (Debug.toString (run program m.program)) ]
|
||||
]
|
||||
|
||||
update : Msg -> Model -> (Model, Cmd Msg)
|
||||
update msg m =
|
||||
case msg of
|
||||
SetProgram prog -> ({ m | program = prog }, Cmd.none)
|
||||
SetQuery query -> ({ m | query = query }, Cmd.none)
|
||||
|
||||
subscriptions : Model -> Sub Msg
|
||||
subscriptions _ = Sub.none
|
||||
@ -78,21 +40,3 @@ main =
|
||||
, update = update
|
||||
, subscriptions = subscriptions
|
||||
}
|
||||
|
||||
-- Latex support:
|
||||
-- Based on https://stackoverflow.com/questions/75492820/embedding-mathematical-equations-in-an-elm-spa
|
||||
|
||||
latex : String -> Html Msg
|
||||
latex expr =
|
||||
Html.node "katex-expression"
|
||||
[ Html.Attributes.attribute "expression" expr
|
||||
, Html.Attributes.attribute "katex-options" (Json.Encode.encode 0 options)
|
||||
]
|
||||
[]
|
||||
|
||||
|
||||
options : Json.Encode.Value
|
||||
options =
|
||||
Json.Encode.object
|
||||
[ ( "displayMode", Json.Encode.bool True )
|
||||
]
|
||||
|
||||
Loading…
Reference in New Issue
Block a user