Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

verbatim -> coq for coq code #1

Draft
wants to merge 1 commit into
base: master
Choose a base branch
from
Draft

verbatim -> coq for coq code #1

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
32 changes: 16 additions & 16 deletions cheat_sheet.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -62,14 +62,14 @@
The first lines of a [.v] file are usually naming the libraries
that will be used to write definitions, statements and prove them,
the syntax, assuming the library [〈lib〉] is installed, is as follow.
<<
[[
From 〈lib〉 Require Import 〈module(s)〉.
>>
]]

For most of the lectures we use simplified versions of the mathcomp library.
<<
[[
From mathcomp Require Import mini_ssreflect 〈other mini mathcomp libs〉.
>>
]]

However, in this cheat sheet, which is more complete, we use:
#<div>#
Expand All @@ -86,34 +86,34 @@ From mathcomp Require Import all_ssreflect.
The keyword [Definition] declares a term, a type, a proposition, or a
non-recursive function. It looks like:

<<
[[
Definition 〈name〉 : 〈type〉 := 〈value〉.
>>
]]

It's possible to omit the [type] if Coq can infer it from the value,
which then looks like:

<<
[[
Definition 〈name〉 := 〈value〉.
>>
]]

But we strongly suggest that you enforce type annotations in
definitions, for the sake of documentation and robustness.

For functions, the arguments can go before or after the colon. That
is, saying:

<<
[[
Definition 〈name〉 : 〈type1〉 -> 〈type2〉 -> 〈type3〉 :=
fun 〈argname〉 〈argname〉 => 〈body〉.

>>
]]
is equivalent to:

<<
[[
Definition 〈name〉 (〈argname〉 : 〈type1〉) : 〈type2〉 -> 〈type3〉 := fun 〈argname〉 => 〈body〉.
Definition 〈name〉 (〈argname〉 : 〈type1〉) (〈argname〉 : 〈type2〉) : 〈type3〉 := 〈body〉.
Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

here

>>
]]

#<div>#
*)
Expand Down Expand Up @@ -204,10 +204,10 @@ End DefinitionExamples.

[Fixpoint] defines a *recursive* function. Syntax is similar to [Definition]:

<<
[[
Fixpoint 〈name〉 : 〈type〉 := fun 〈arguments...〉 => 〈body〉.
Fixpoint 〈name〉 (〈argname〉 : 〈type〉) (argname : 〈type〉) ... : 〈type〉 := 〈body〉.
>>
]]

Such a definition is accepted if termination is ensured by a recursive call
on a strict subterm.
Expand Down Expand Up @@ -250,12 +250,12 @@ End FixpointExamples.

The syntax looks like:

<<
[[
Lemma 〈name〉 : 〈proof statement〉.
Proof.
〈proof body〉
Qed.
>>
]]

[Theorem], [Remark], [Corollary] are synonyms.

Expand Down