lib-nested/nested/src/editors
2023-08-25 04:00:38 +02:00
..
char cargo fix 2023-08-21 16:31:44 +02:00
integer cargo fix 2023-08-21 16:31:44 +02:00
list wip typterm edit; list editor: split using spill buf 2023-08-25 04:00:38 +02:00
product cargo fix 2023-08-21 16:31:44 +02:00
sum node: adapt new() to always initialize ctx and data; fix get_morphism bug 2023-08-15 23:18:51 +02:00
typeterm wip typterm edit; list editor: split using spill buf 2023-08-25 04:00:38 +02:00
mod.rs move TypeTerm editor to editors module; remove make_editor.rs and distribute context initialization into editor submodules 2023-08-21 15:49:07 +02:00