Я ищу инструмент (желательно GUI, но CLI будет работать), который позволяет мне вводить математические выражения, а затем выполнять манипуляции с ними, но ограничивает меня только математически допуст
У меня есть определенные индуктивные типы: Inductive InL (A:Type) (y:A) : list A -> Prop :=
| InHead : forall xs:list A, InL y (cons y xs)
| InTail : forall (x:A) (xs:list A), InL y xs -> In