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

Add some forward-only arithmetic operations and make rho render as LaTeX

Browse Source 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin 2024-09-15 16:33:07 -07:00
parent e7d3e840b3
commit c77bb6f900
2 changed files with 6 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
src/Bergamot/Latex.elm
View File

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

4
src/Bergamot/Rules.elm
View File

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