Functional Programming & Proofs
Trees and languages
- (
rec
ursive datayes, trees, abstract syntax)
How to define set of boolean expressions
?
- How to
print
or evaluate
boolean expressions ?
type BExp = BVal of Bool | BNot of BExp | BAnd of BExp*BExp;;
let rec beval be =
match be with
| BVal v -> v
| BNot be1 -> Not (beval be1)
| BAnd (be1,be2) -> And (beval be1) (beval be2);;
let be = BAnd (BVal True,BNot (BVal False));;
beval be;;
let rec bstring be =
match be with
| BVal True -> "True"
| BVal False -> "False"
| BNot be1 -> "(Not "+(bstring be1)+")"
| BAnd (be1,be2) -> (bstring be1)+" <&> "+(bstring be2);;
(bstring be)," = ", (beval be);;
printfn "%s = %A" (bstring be) (beval be);;
4 - 10
docteur dr laurent thiry uha mulhouse france functional programming fsharp proof theory coq coqide
docteur dr laurent thiry uha mulhouse france functional programming fsharp proof theory coq coqide
docteur dr laurent thiry uha mulhouse france functional programming fsharp proof theory coq coqide
docteur dr laurent thiry uha mulhouse france functional programming fsharp proof theory coq coqide
docteur dr laurent thiry uha mulhouse france functional programming fsharp proof theory coq coqide
docteur dr laurent thiry uha mulhouse france functional programming fsharp proof theory coq coqide
docteur dr laurent thiry uha mulhouse france functional programming fsharp proof theory coq coqide
docteur dr laurent thiry uha mulhouse france functional programming fsharp proof theory coq coqide
docteur dr laurent thiry uha mulhouse france functional programming fsharp proof theory coq coqide
docteur dr laurent thiry uha mulhouse france functional programming fsharp proof theory coq coqide
docteur dr laurent thiry uha mulhouse france functional programming fsharp proof theory coq coqide