pl/frap
1
0
Fork 0
mirror of https://github.com/achlipala/frap.git synced 2025-03-19 11:12:28 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

Merge pull request #25 from bmsherman/fix_minus

Browse source 
minus notation should be for subtraction, not set minus
This commit is contained in:
Adam Chlipala 2018-04-26 08:17:14 -04:00 • committed by GitHub
commit 79db2ea024
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
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.