pl/frap
1
0
Fork 0
mirror of https://github.com/achlipala/frap.git synced 2024-11-28 07:16:20 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

Get rid of the “reset” scope in HoareLogic.v

Browse source 
It's not needed, and it makes everything harder to read.
This commit is contained in:
Clément Pit-Claudel 2021-04-12 15:04:56 -04:00
parent 1664ddb531
commit 2ed1d52171
2 changed files with 2 additions and 19 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
HoareLogic.v
View file

@ -191,20 +191,11 @@ Notation "'when' b 'then' then_ 'else' else_ 'done'" := (If_ b then_ else_) (at
Notation "{{ I }} 'while' b 'loop' body 'done'" := (While_ I b body) (at level 75). Notation "{{ I }} 'while' b 'loop' body 'done'" := (While_ I b body) (at level 75).
Notation "'assert' {{ I }}" := (Assert I) (at level 75). Notation "'assert' {{ I }}" := (Assert I) (at level 75).
Delimit Scope cmd_scope with cmd. Delimit Scope cmd_scope with cmd.
(*Declare Scope reset_scope.*)
Infix "+" := plus : reset_scope.
Infix "-" := Init.Nat.sub : reset_scope.
Infix "*" := mult : reset_scope.
Infix "=" := eq : reset_scope.
Infix "<" := lt : reset_scope.
Delimit Scope reset_scope with reset.
Open Scope reset_scope.
(* END macros *) (* END macros *)
(* We should draw some attention to the next notation, which defines special (* We should draw some attention to the next notation, which defines special
* lambdas for writing assertions. *) * lambdas for writing assertions. *)
Notation "h & v ~> e" := (fun h v => e%reset) (at level 85, v at level 0). Notation "h & v ~> e" := (fun h v => e%nat%type) (at level 85, v at level 0).
(* And here's the classic notation for Hoare triples. *) (* And here's the classic notation for Hoare triples. *)
Notation "{{ P }} c {{ Q }}" := (hoare_triple P c%cmd Q) (at level 90, c at next level). Notation "{{ P }} c {{ Q }}" := (hoare_triple P c%cmd Q) (at level 90, c at next level).

10
HoareLogic_template.v
View file

@ -162,19 +162,11 @@ Notation "'when' b 'then' then_ 'else' else_ 'done'" := (If_ b then_ else_) (at
Notation "{{ I }} 'while' b 'loop' body 'done'" := (While_ I b body) (at level 75). Notation "{{ I }} 'while' b 'loop' body 'done'" := (While_ I b body) (at level 75).
Notation "'assert' {{ I }}" := (Assert I) (at level 75). Notation "'assert' {{ I }}" := (Assert I) (at level 75).
Delimit Scope cmd_scope with cmd. Delimit Scope cmd_scope with cmd.
Infix "+" := plus : reset_scope.
Infix "-" := Init.Nat.sub : reset_scope.
Infix "*" := mult : reset_scope.
Infix "=" := eq : reset_scope.
Infix "<" := lt : reset_scope.
Delimit Scope reset_scope with reset.
Open Scope reset_scope.
(* END macros *) (* END macros *)
(* We should draw some attention to the next notation, which defines special (* We should draw some attention to the next notation, which defines special
* lambdas for writing assertions. *) * lambdas for writing assertions. *)
Notation "h & v ~> e" := (fun h v => e%reset) (at level 85, v at level 0). Notation "h & v ~> e" := (fun h v => e%nat%type) (at level 85, v at level 0).
(* And here's the classic notation for Hoare triples. *) (* And here's the classic notation for Hoare triples. *)
Notation "{{ P }} c {{ Q }}" := (hoare_triple P c%cmd Q) (at level 90, c at next level). Notation "{{ P }} c {{ Q }}" := (hoare_triple P c%cmd Q) (at level 90, c at next level).