|
|
11dd5ee9fd
|
Put render rules separately from regular rules
This should let us hide them from the user and maybe speed up rendering
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2023-12-02 00:25:23 -08:00 |
|
|
|
1d3f3fd3f8
|
Use 'lazy' to speed up re-rendering
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2023-12-02 00:07:01 -08:00 |
|
|
|
12fa4dc1fd
|
WIP: Use bergamot to render inference rules.
Not the proof trees yet, but it should be about the same.
|
2023-12-01 23:31:43 -08:00 |
|
|
|
45a04cc59c
|
Add a mode for entering the object language to parse
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2023-12-01 11:31:38 -08:00 |
|
|
|
51c78af138
|
Add an initial parser for the Bergamot 'object language'
|
2023-11-30 22:44:20 -08:00 |
|
|
|
d9f9522365
|
Add a tab to switch between editor and rendered view
|
2023-11-30 21:29:37 -08:00 |
|
|
|
bb18c8bd8c
|
Tweak the HTML tags generated by Bergamot.
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2023-11-29 22:20:55 -08:00 |
|
|
|
9d287a37d5
|
Add flags for setting rules and query before starting
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2023-11-26 20:53:31 -08:00 |
|
|
|
ff1ea05784
|
Add yielding to help proof search
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2023-11-26 17:17:10 -08:00 |
|
|
|
33c3f87564
|
Add some styling (still very early stages)
|
2023-11-26 16:25:23 -08:00 |
|
|
|
acc769e799
|
Add LaTeX support for rendering rules
|
2023-11-26 15:54:01 -08:00 |
|
|
|
7cc5d05e9c
|
Add a way to print the rules as LaTeX
|
2023-11-26 14:34:52 -08:00 |
|
|
|
e123f24af0
|
Add support for reifying proof trees
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2023-11-26 13:14:44 -08:00 |
|
|
|
985be53367
|
Add an interactive 'can this query be satisfied' interface
|
2023-11-26 12:47:05 -08:00 |
|
|
|
efe0efbee7
|
Add a (debug) interactive demo
|
2023-11-26 11:58:20 -08:00 |
|
|
|
800c96dc7b
|
Add an initial Main.elm file
|
2023-11-26 11:43:38 -08:00 |
|
