Add a new builtin to identify symbols
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
parent
012c1b0d0c
commit
a1ae15d84c
|
@ -135,6 +135,9 @@ builtinRules t =
|
||||||
Call "str" [StringLit s] ->
|
Call "str" [StringLit s] ->
|
||||||
MkProofTree { name = "BuiltinStr", conclusion = t, premises = [] }
|
MkProofTree { name = "BuiltinStr", conclusion = t, premises = [] }
|
||||||
|> pure
|
|> pure
|
||||||
|
Call "sym" [Call s []] ->
|
||||||
|
MkProofTree { name = "BuiltinSym", conclusion = t, premises = [] }
|
||||||
|
|> pure
|
||||||
Call "tostring" [IntLit i, Var output] ->
|
Call "tostring" [IntLit i, Var output] ->
|
||||||
liftUnification unify (Var output) (StringLit (String.fromInt i))
|
liftUnification unify (Var output) (StringLit (String.fromInt i))
|
||||||
|> map (\_ -> MkProofTree { name = "BuiltinToString", conclusion = t, premises = []})
|
|> map (\_ -> MkProofTree { name = "BuiltinToString", conclusion = t, premises = []})
|
||||||
|
|
Loading…
Reference in New Issue
Block a user