blob: eaba8a0ab6f740b3f9af3fb85f459fb8c2a75f0a (
about) (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
|
From mininix Require Export evallang.interp.
From stdpp Require Import options.
Import evallang.
Definition interp' (n : nat) (s : string) : res val :=
interp n ∅ (EEval ∅ (EString s)).
Lemma test_1_a : interp' 1000 ("(x: x) ""s""") = mret (VString "s").
Proof. by vm_compute. Qed.
Lemma test_1_b : interp' 1000 ("(""x"": x) ""s""") = mret (VString "s").
Proof. by vm_compute. Qed.
Lemma test_1_c : interp' 1000 ("((y:y) ""x"": x) ""s""") = mret (VString "s").
Proof. by vm_compute. Qed.
Lemma test_1_d : interp' 1000 ("(((y:y) ""x""): x) ""s""") = mret (VString "s").
Proof. by vm_compute. Qed.
Lemma test_2 : interp' 1000 ("(x: y: eval! y) ""s"" ""x""") = mret (VString "s").
Proof. by vm_compute. Qed.
Lemma test_3 : interp' 1000 ("eval! ""x: x"" ""s""") = mret (VString "s").
Proof. by vm_compute. Qed.
Lemma test_4_a :
interp' 1000 ("(x: y: eval! y) ""s"" ""x""") = mret (VString "s").
Proof. by vm_compute. Qed.
Lemma test_4_b :
interp' 1000 ("eval! ""(x: y: eval! y) \""s\"" \""x\""""") = mret (VString "s").
Proof. by vm_compute. Qed.
Lemma test_5 :
interp' 1000 ("(x: y: eval! ""x: x"" (eval! y)) ""s"" ""x""") = mret (VString "s").
Proof. by vm_compute. Qed.
|
