Я прочитал довольно много о определении типа данных в Изабеллу, как, например,Инициализировать типы данных в Isabelle
datatype_new bst = Leaf int | Node int bst bst
или
datatype 'a list = Nil | Cons 'a "'a list"
Однако, я не нахожу никаких примеров, как заполнить эти типы данных с данные, например, если вы хотите, чтобы список был инициализирован размером 10 и всеми значениями.
Вот список размером 10 и значением 0:
definition "lots_of_10s = Cons 0 (Cons 0 (Cons 0 (Cons 0 (Cons 0 (Cons 0 (Cons 0 (Cons 0 (Cons 0 (Cons 0 Nil)))))))))"
Я получаю внутреннюю синтаксическую ошибку, если я попробую это. Как бы определение было для bst? – user2057890
Можете ли вы написать что-то вроде определения «bst 1 :: int 2 :: int 3 :: int» – user2057890
'bst' - это тип, а не конструктор. Вероятно, вы имеете в виду «Узел 1 (лист 2) (лист 3)). Но у меня создается впечатление, что вы, возможно, захотите вернуться к учебнику для начинающих по программированию в Isabelle. –
Раньше вы задавали конкретный вопрос, и я дал точный ответ, за которым последовало некоторое проповедование, что является моим основным способом злоупотребления форматом SO. SO - формат вопрос-ответ. Вы задаете вопрос, кто-то пытается ответить. Люди должны задавать некоторые вопросы. Здесь кто-то еще сделал уценку для вашего кода. Каждая область нуждается в полиции самостоятельно, поэтому вопросы остаются достойными качествами. Сегодня, подумайте, полиция, что бы это ни стоило, но отвратительно. Что касается 'list', я вижу на странице 1018 и стр. 9 двух IsaDocs, как создать инициализированный список. Осмотреться. Вы можете найти их. –