From c77bb6f900f2ca4a1a916e66adf564032956cb6b Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Sun, 15 Sep 2024 16:33:07 -0700 Subject: [PATCH] Add some forward-only arithmetic operations and make rho render as LaTeX Signed-off-by: Danila Fedorin --- src/Bergamot/Latex.elm | 3 ++- src/Bergamot/Rules.elm | 4 ++++ 2 files changed, 6 insertions(+), 1 deletion(-) diff --git a/src/Bergamot/Latex.elm b/src/Bergamot/Latex.elm index 683f1cb..d4909f5 100644 --- a/src/Bergamot/Latex.elm +++ b/src/Bergamot/Latex.elm @@ -68,4 +68,5 @@ metavariableToLatex (MkMetavariable s) = noQuestion = String.dropLeft 1 s in if String.startsWith "tau" noQuestion then "\\" ++ noQuestion else - if String.startsWith "Gamma" noQuestion then "\\" ++ noQuestion else noQuestion + if String.startsWith "Gamma" noQuestion then "\\" ++ noQuestion else + if String.startsWith "rho" noQuestion then "\\" ++ noQuestion else noQuestion diff --git a/src/Bergamot/Rules.elm b/src/Bergamot/Rules.elm index d2cb507..b05ac9f 100644 --- a/src/Bergamot/Rules.elm +++ b/src/Bergamot/Rules.elm @@ -158,6 +158,10 @@ builtinRules t = Call "int" [Var output] -> let rec i = interleave (suggest "BuiltinInt" (IntLit i) output) (lazy <| \_ -> rec (i+1)) in rec 0 + Call "add" [IntLit i1, IntLit i2, Var output] -> + suggest "BuiltinAdd" (IntLit (i1 + i2)) output + Call "subtract" [IntLit i1, IntLit i2, Var output] -> + suggest "BuiltinSubtract" (IntLit (i1 - i2)) output Call "float" [FloatLit f] -> MkProofTree { name = "BuiltinFloat", conclusion = t, premises = [] } |> pure