Yiming Xu (Sep 12 2024 at 08:35): Yiming Xu (Sep 12 2024 at 08:35):I am trying to define substitution of variables (into formulas) by recursion on constructors. And encounter the following syntax error:
image.png
What is wrong here?
Yiming Xu (Sep 12 2024 at 08:35):datatype form = VAR "num"
| FALSE
| DISJ "form" "form"
| NOT "form"
| DIAM "form"
fun subst :: "(num ⇒ form) ⇒ form ⇒ form"
where
| "subst s FALSE = FALSE"
| "subst s (VAR p) = s p"
| "subst s (DISJ f1 f2) = DISJ (subst s f1) (subst s f2)"
| "subst s (NOT f) = NOT (subst s f)"
| "subst s (DIAM f) = DIAM (subst s f)"
no | before the first pattern
Yiming Xu (Sep 12 2024 at 08:40):Oh thanks, my stupid.
Last updated: Dec 21 2024 at 16:20 UTC