pl/frap
1
0
Fork 0
mirror of https://github.com/achlipala/frap.git synced 2024-12-01 00:26:18 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

minus notation should be for subtraction, not set minus

Browse source
This commit is contained in:
Ben Sherman 2018-04-25 22:28:22 -04:00
parent b7fd72f309
commit fa4d8ca8db
2 changed files with 4 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
HoareLogic.v
View file

@ -6,6 +6,8 @@
Require Import Frap. Require Import Frap.
(** * Syntax and semantics of a simple imperative language *) (** * Syntax and semantics of a simple imperative language *)
(* Here's some appropriate syntax for expressions (side-effect-free) of a simple (* Here's some appropriate syntax for expressions (side-effect-free) of a simple
@ -188,7 +190,7 @@ 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 "+" := plus : reset_scope.
Infix "-" := minus : reset_scope. Infix "-" := Init.Nat.sub : reset_scope.
Infix "*" := mult : reset_scope. Infix "*" := mult : reset_scope.
Infix "=" := eq : reset_scope. Infix "=" := eq : reset_scope.
Infix "<" := lt : reset_scope. Infix "<" := lt : reset_scope.

2
HoareLogic_template.v
View file

@ -164,7 +164,7 @@ 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 "+" := plus : reset_scope.
Infix "-" := minus : reset_scope. Infix "-" := Init.Nat.sub : reset_scope.
Infix "*" := mult : reset_scope. Infix "*" := mult : reset_scope.
Infix "=" := eq : reset_scope. Infix "=" := eq : reset_scope.
Infix "<" := lt : reset_scope. Infix "<" := lt : reset_scope.