Skip to content

Commit

Permalink
Fix some more proofs
Browse files Browse the repository at this point in the history
  • Loading branch information
@myreen
myreen committed Nov 24, 2021
1 parent 1891e85 commit 3ae2206
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions basis/TextIOProofScript.sml
View file
Expand Up @@ -7357,7 +7357,7 @@ Proof
\\ gs[] \\ simp[libTheory.the_def,AFUPDKEY_ALOOKUP,MAX_DEF])
\\ conj_tac
>- (gs[get_mode_def,fastForwardFD_def,get_file_content_def]
\\ PairCases_on ‘z’
\\ PairCases_on ‘x'’

This comment has been minimized.

Sign in to view

Copy link
@mn200

mn200 Nov 25, 2021

Contributor

Using rename would surely be more robust

This comment has been minimized.

Sign in to view

Copy link
@myreen

myreen Nov 25, 2021

Author Contributor

You are of course right. That was sloppy of me. I'll insert a rename.
\\ qmatch_assum_rename_tac ‘ALOOKUP _ _ = SOME (ino,mode,off')’
\\ gs[] \\ simp[libTheory.the_def,AFUPDKEY_ALOOKUP])
\\ xsimpl \\ simp[fastForwardFD_eq_forwardFD] \\ xsimpl
Expand Down Expand Up @@ -7633,7 +7633,7 @@ Proof
\\ gs[] \\ simp[libTheory.the_def,AFUPDKEY_ALOOKUP,MAX_DEF])
\\ conj_tac
>- (gs[get_mode_def,fastForwardFD_def,get_file_content_def]
\\ PairCases_on ‘z’
\\ PairCases_on ‘x'’
\\ qmatch_assum_rename_tac ‘ALOOKUP _ _ = SOME (ino,mode,off')’
\\ gs[] \\ simp[libTheory.the_def,AFUPDKEY_ALOOKUP])
\\ xsimpl \\ simp[fastForwardFD_eq_forwardFD] \\ xsimpl
Expand Down

0 comments on commit 3ae2206

Please sign in to comment.