Skip to content
Permalink
Browse files

Rename to AFUPDKEY and ADELKEY

  • Loading branch information...
xrchz committed May 3, 2019
1 parent 0aea6df commit 45a84e07ec595193a2d3bacd455722f180ec814c

Large diffs are not rendered by default.

Oops, something went wrong.
@@ -144,9 +144,9 @@ Theorem extract_fs_with_numchars_keeps_iostreams
fsFFITheory.openFile_def,
fsFFITheory.write_def]
\\ TRY pairarg_tac \\ fs[]
\\ rveq \\ fs[ALOOKUP_ALIST_DELKEY, fsFFIPropsTheory.bumpFD_forwardFD]
\\ rveq \\ fs[ALOOKUP_ADELKEY, fsFFIPropsTheory.bumpFD_forwardFD]
\\ fs[CaseEq"bool"]
\\ rfs[fsFFITheory.fsupdate_def, fsFFIPropsTheory.forwardFD_def, ALIST_FUPDKEY_ALOOKUP]
\\ rfs[fsFFITheory.fsupdate_def, fsFFIPropsTheory.forwardFD_def, AFUPDKEY_ALOOKUP]
\\ fs[CaseEq"option"]
\\ fs[CaseEq"bool"]
\\ Cases_on`v` \\ fs[]
@@ -192,8 +192,8 @@ Theorem extract_fs_with_numchars_closes_iostreams
fsFFITheory.openFile_def,
fsFFITheory.write_def]
\\ TRY pairarg_tac \\ fs[]
\\ rveq \\ fs[ALOOKUP_ALIST_DELKEY, fsFFITheory.bumpFD_def, ALIST_FUPDKEY_ALOOKUP]
\\ rw[fsFFITheory.fsupdate_def, ALIST_FUPDKEY_ALOOKUP]
\\ rveq \\ fs[ALOOKUP_ADELKEY, fsFFITheory.bumpFD_def, AFUPDKEY_ALOOKUP]
\\ rw[fsFFITheory.fsupdate_def, AFUPDKEY_ALOOKUP]
\\ PURE_CASE_TAC \\ fs[CaseEq"option"]
\\ CCONTR_TAC \\ fs[]);

@@ -230,7 +230,7 @@ Theorem extract_stdo_extract_fs
\\ rw[IO_fs_component_equality]
\\ qpat_assum`ALOOKUP fs.files _ = _`mp_tac
\\ qpat_assum`fs.files = _`SUBST1_TAC
\\ simp[ALIST_FUPDKEY_ALOOKUP] )
\\ simp[AFUPDKEY_ALOOKUP] )
\\ Cases
\\ rw[extract_fs_def,extract_stdo_def]
>- (
@@ -253,7 +253,7 @@ Theorem extract_stdo_extract_fs
\\ fs[stdo_def]
\\ simp[Abbr`fs'`,fsupdate_def]
\\ CASE_TAC \\ fs[]
\\ simp[ALIST_FUPDKEY_ALOOKUP]
\\ simp[AFUPDKEY_ALOOKUP]
\\ ...)
\\ qpat_x_assum`_ = SOME _`mp_tac
Oops, something went wrong.

0 comments on commit 45a84e0

Please sign in to comment.
You can’t perform that action at this time.