Advent-of-Code/AdventOfCode-2020
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Compare commits

base: Advent-of-Code:2b69cbd391398ed21ccf3b2b06d62dc46207fe85
Branches Tags
Advent-of-Code:master
..
compare: Advent-of-Code:7a8503c3fe1aa7e624e4d8672aa9b56d24b4ba82
Branches Tags
Advent-of-Code:master

1 Commits
2b69cbd391 ... 7a8503c3fe

Author SHA1 Message Date
Danila Fedorin
7a8503c3fe Use auto instead of apply. 2021-01-02 21:22:07 -08:00
1 changed files with 2 additions and 2 deletions
Expand all files Collapse all files

4
day8.v
View File

@@ -235,9 +235,9 @@ Module DayEight (Import M:Int).
intros pc acc. intros pc acc.
destruct (valid_input_progress pc l acc) as [[_ Hd]|[pc' [Hw [[_ Hst]|[pc'' [acc'' [Hin Hst]]]]]]]. destruct (valid_input_progress pc l acc) as [[_ Hd]|[pc' [Hw [[_ Hst]|[pc'' [acc'' [Hin Hst]]]]]]].
- (* We're done. *) - (* We're done. *)
eexists. apply run_noswap_ok. apply Hd. eexists. apply run_noswap_ok. assumption.
- (* We're stuck. *) - (* We're stuck. *)
eexists. apply run_noswap_fail. apply Hst. eexists. apply run_noswap_fail. assumption.
- (* We can make a step. This will remove our current PC from the valid list, *) - (* We can make a step. This will remove our current PC from the valid list, *)
edestruct (H (set_remove Fin.eq_dec pc' l)). edestruct (H (set_remove Fin.eq_dec pc' l)).
(* Since the PC must be in the list, removing it makes the list smaller. *) (* Since the PC must be in the list, removing it makes the list smaller. *)