2022-03-02 17:02:51 -05:00
|
|
|
{-# OPTIONS --rewriting #-}
|
|
|
|
|
2022-02-09 18:14:29 -05:00
|
|
|
module Examples.OpSem where
|
|
|
|
|
|
|
|
open import Luau.OpSem using (_⊢_⟶ᴱ_⊣_; _⊢_⟶ᴮ_⊣_; subst)
|
2022-03-02 17:02:51 -05:00
|
|
|
open import Luau.Syntax using (Block; var; val; nil; local_←_; _∙_; done; return; block_is_end)
|
2022-02-11 20:03:26 -05:00
|
|
|
open import Luau.Heap using (∅)
|
2022-02-09 18:14:29 -05:00
|
|
|
|
2022-03-02 17:02:51 -05:00
|
|
|
ex1 : ∅ ⊢ (local (var "x") ← val nil ∙ return (var "x") ∙ done) ⟶ᴮ (return (val nil) ∙ done) ⊣ ∅
|
|
|
|
ex1 = subst nil
|