Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Tej Chajed
stdpp
Commits
91b86f56
Commit
91b86f56
authored
Feb 08, 2018
by
Robbert Krebbers
Browse files
Make `nat_cancel` comments Coqdoc.
parent
fc7ddaf7
Changes
1
Hide whitespace changes
Inline
Side-by-side
theories/nat_cancel.v
View file @
91b86f56
From
stdpp
Require
Import
numbers
.
(* The class [NatCancel m n m' n'] is a simple canceler for natural numbers
(*
*
The class [NatCancel m n m' n'] is a simple canceler for natural numbers
implemented using type classes.
Input: [m], [n]; output: [m'], [n'].
...
...
@@ -71,7 +71,7 @@ Global Instance nat_cancel_leaf_S_else m n m' n' :
NatCancelLeaf
m
n
m'
n'
→
NatCancelLeaf
m
(
S
n
)
m'
(
S
n'
)
|
4
.
Proof
.
unfold
NatCancelLeaf
,
NatCancel
.
omega
.
Qed
.
(* The instance [nat_cancel_S_both] is redundant, but may reduce proof search
(*
*
The instance [nat_cancel_S_both] is redundant, but may reduce proof search
quite a bit, e.g. when canceling constants in constants. *)
Global
Instance
nat_cancel_S_both
m
n
m'
n'
:
NatCancel
m
n
m'
n'
→
NatCancel
(
S
m
)
(
S
n
)
m'
n'
|
1
.
...
...
@@ -83,4 +83,4 @@ Proof. unfold NatCancel, MakeNatPlus. omega. Qed.
Global
Instance
nat_cancel_S
m
m'
m''
Sm'
n
n'
n''
:
NatCancel
m
n
m'
n'
→
NatCancelLeaf
1
n'
m''
n''
→
MakeNatS
m''
m'
Sm'
→
NatCancel
(
S
m
)
n
Sm'
n''
|
3
.
Proof
.
unfold
NatCancelLeaf
,
NatCancel
,
MakeNatS
.
omega
.
Qed
.
\ No newline at end of file
Proof
.
unfold
NatCancelLeaf
,
NatCancel
,
MakeNatS
.
omega
.
Qed
.
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment