maude in relation coq
Opened this issue · 1 comments
brando90 commented
'
Module aevalR_first_try.
Inductive aevalR : aexp → nat → Prop :=
| E_ANum : ∀ (n: nat),
aevalR (ANum n) n
| E_APlus : ∀ (e1 e2: aexp) (n1 n2: nat),
aevalR e1 n1 →
aevalR e2 n2 →
aevalR (APlus e1 e2) (n1 + n2)
| E_AMinus: ∀ (e1 e2: aexp) (n1 n2: nat),
aevalR e1 n1 →
aevalR e2 n2 →
aevalR (AMinus e1 e2) (n1 - n2)
| E_AMult : ∀ (e1 e2: aexp) (n1 n2: nat),
aevalR e1 n1 →
aevalR e2 n2 →
aevalR (AMult e1 e2) (n1 * n2)
'
maude translates to above