Open brando90 opened 5 years ago
' 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
https://softwarefoundations.cis.upenn.edu/lf-current/Imp.html
' 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