From 2c39e53ab0809225cc86057588912ba20390162a Mon Sep 17 00:00:00 2001 From: aqjune Date: Thu, 17 May 2018 17:51:46 +0900 Subject: [PATCH] Update README.md --- README.md | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/README.md b/README.md index 8b35026..84224e3 100644 --- a/README.md +++ b/README.md @@ -47,7 +47,7 @@ def bigstep_both:= ∀ ss se (p:program) oss' ose' η -- Its proof is at equiv.lean ``` -2. We can generate initial state correctly: +2. We can generate initial state correctly. ``` def init_state_encode:= ∀ (freevars:list (string × ty)) (sg sg':std_gen) ise iss @@ -70,10 +70,10 @@ def refines_single_reg_correct := ∀ (psrc ptgt:program) -- Its proof is at refinement.lean ``` -- TODO: +- TODO - Connect this with `check_single_reg`, which allows a target program to - use definitions in the source program for convenience. - - Check that `freevars.get` correctly returns all free variables. + use definitions in the source program for convenience + - Check that `freevars.get` correctly returns all free variables - Connect this with correctness criteria in Alive paper # Contributing