lib-nested/nested/src/editors
2023-08-21 15:49:07 +02:00
..
char 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
integer 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
list 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
product restructure TypeTerm 2023-08-12 19:03:14 +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 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
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