La maggior parte degli assistenti di prova sono linguaggi di programmazione funzionale con tipi dipendenti. Possono provare programmi/algoritmi. Mi interessa, invece, l'assistente di prova adatto al m
Finora ho scritto dimostrazioni per assurdo nello stile seguito a Isabelle (utilizzando un modello da Jeremy Siek): lemma "<expression>"
proof -
{
assume "¬ <expression>"
then have Fal