Как написать эту функцию в SML

Question

Я пытаюсь написать функцию в Isabelle для некоторых задач в задании , и я хотел убедиться, что моя функция работает правильно, поэтому я подумал о , проверяя ее на SML, но могу Кажется, он не может понять, как его написать. I никогда не использовали/писали/не изучали функциональное программирование, поэтому у меня есть небольшая проблема с ним. Может ли кто-нибудь помочь мне или, может быть, если что-то в Изабелле про тестирование , как работает функция, он может указать мне на правильное направление?

функции является следующим и в основном удаление первого появления элемента в списке и удаление всех вхождений из списка

fun del1:: "'a ⇒ 'a list ⇒ 'a list" where 
    "del1 a Nil = Nil" | 
    "del1 a (x#xs) = (if x = a then xs else x#(del1 a xs))" 


fun delall:: "'a ⇒ 'a list ⇒ 'a list" where 
    "delall a Nil = Nil" | 
    "delall a (x#xs) = (if x = a then (delall a xs) else x#(delall a xs))" 

Answer 1

Я не совсем уверен, получу ли я на ваш вопрос. Во-первых, синтаксис Isabelle/HOL и SML не очень разные. Если вы просто хотите, чтобы получить варианты вашей функции в SML, вероятно, самый быстрый способ использует генератор кода Изабель

export_code del1 delall in SML 

что приводит к чему-то вроде

fun del1 A_ a [] = [] 
    | del1 A_ a (x :: xs) = (if HOL.eq A_ x a then xs else x :: del1 A_ a xs); 

fun delall A_ a [] = [] 
    | delall A_ a (x :: xs) = 
    (if HOL.eq A_ x a then delall A_ a xs else x :: delall A_ a xs); 

Однако, поскольку это содержит некоторые Isabelle конкретные вещи (как словарная конструкция, чтобы избавиться от классов типа) может быть, вы предпочитаете рукописный код:

fun del1 a [] = [] 
    | del1 a (x::xs) = if x = a then xs else x :: (del1 a xs) 

fun delall a [] = [] 
    | delall a (x::xs) = if x = a then delall a xs else x :: delall a xs 

с другой стороны, если вы просто хотите попробовать свой Functio ns на некоторых входах, вы можете сделать это внутри Isabelle, используя value. НАПРИМЕР,

value "del1 (2::nat) [1, 2 , 3]" 
value "delall ''x'' [''x'', ''y'', ''z'', ''q'', ''x'']" 

Answer 2

Существует мало, чтобы добавить к ответу Крис, только эту деталь: В Isabelle2013-2 Документации панель Isabelle/jEdit имеет несколько примеров QuickStart. Это включает в себя src/HOL/ex/ML.thy, который показывает немного Isabelle/HOL как логический язык и SML как функциональный язык, а также некоторые связи между ними.