I hereby claim:
- I am glimonta on github.
- I am glimonta (https://keybase.io/glimonta) on keybase.
- I have a public key ASC2_ZU6tk7bag_kDpAEnHKLmPdT8g23KWgGsrlueV3Wmgo
To claim this, I am signing this object:
I hereby claim:
To claim this, I am signing this object:
lemma "eval (Ref e) s = do { | |
(v, s) ← eval_l e s; | |
(case v of (A _) ⇒ Some (v, s) | _ ⇒ None) | |
}" | |
lemma "eval_l (Derefl e) s = do { | |
(v, s) ← eval e s; | |
(case v of (A _) ⇒ Some (v, s) | _ ⇒ None) | |
}" |
fun eval :: "exp ⇒ state ⇒ (val × state) option" | |
and eval_l :: "lexp ⇒ state ⇒ (val × state) option" where | |
"eval (Const c) s = Some (c, s)" | |
| "eval Null s = Some (NullVal, s)" | |
| "eval (V x) (σ, μ) = Some (σ x, (σ, μ))" | |
| "eval (Plus i⇩1 i⇩2) s = do { | |
(v⇩1, s) ← eval i⇩1 s; | |
(v⇩2, s) ← eval i⇩2 s; | |
v ← plus_val v⇩1 v⇩2; | |
Some (v, s) |
{-# LANGUAGE UnicodeSyntax #-} | |
{-# LANGUAGE FlexibleInstances #-} | |
{-# LANGUAGE Rank2Types #-} | |
import Data.List (nub, subsequences) | |
import Data.List.Unicode ((∈)) | |
import Data.Functor ((<$>)) | |
infixr 3 ∧ | |
infixr 2 ∨ |
{-# LANGUAGE UnicodeSyntax #-} | |
{-# LANGUAGE DeriveDataTypeable #-} | |
import Control.Applicative (pure) | |
import Data.Data (Data) | |
import Data.Data.Lens (template) | |
import Data.Functor ((<$>)) | |
import Data.List (nub, subsequences) | |
import Data.List.Unicode ((∈)) | |
import Data.Typeable (Typeable) |