issues
search
math-comp
/
mcb
Mathematical Components (the Book)
Other
140
stars
25
forks
source link
issues
Newest
Newest
Most commented
Recently updated
Oldest
Least commented
Least recently updated
Misc. corrections
#54
anton-trunov
closed
6 years ago
2
Sect. 1.3.3 Option and pair data types: introduce irrefutable pattern-matching?
#53
anton-trunov
closed
6 years ago
1
Sect. 1.3.3 Option and pair data types: pair type is called prod in Coq
#52
anton-trunov
closed
6 years ago
0
Sect. 1.2 Data types, first examples: confusing paragraphs
#51
anton-trunov
closed
5 years ago
0
"Eval compute in" vs "Compute" ?
#50
anton-trunov
closed
6 years ago
8
Conventions: advice vs tricky details
#49
anton-trunov
closed
6 years ago
0
Pr
#48
whxvd
closed
6 years ago
1
Ch. 6: (n : nat) + (i : ’I_7) can't be smaller than 7
#47
anton-trunov
closed
6 years ago
1
Many small changes, deeper question on link between leq and subn
#46
ybertot
closed
6 years ago
1
small improvements to the introduction
#45
ybertot
closed
6 years ago
0
§1.3p31: explanation of n-ary operations uses different separation symbol for the text and the example
#44
dvberkel
closed
5 years ago
2
Web ver?
#43
takasimiz
opened
6 years ago
0
added missing \C{}
#42
CohenCyril
closed
6 years ago
0
§2.4: the main goal actually mentions the “divides” predicate
#41
mituharu
closed
6 years ago
1
§2.3.1: explanation of "commutative" not updated
#40
mituharu
closed
6 years ago
1
§2.3.1: (rel T) explained, but no longer used
#39
mituharu
closed
6 years ago
1
Avoid introducing subn in chProgramming
#38
ybertot
closed
3 years ago
1
corrections and more marginal notes
#37
ybertot
closed
7 years ago
1
Suggestions on Chap. 2
#36
remysucre
closed
7 years ago
3
overlapping margin notes on p. 25
#35
remysucre
closed
7 years ago
2
corrections for phantom
#34
mituharu
closed
7 years ago
1
Minor corrections for seq separators.
#33
mituharu
closed
6 years ago
1
refining b13c374 and f8adc58
#32
darijgr
closed
7 years ago
5
modifs on equational theories
#31
ybertot
closed
7 years ago
2
Some minor corrections
#30
darijgr
closed
3 years ago
1
add a guideline for end of sentences
#29
ybertot
closed
7 years ago
0
Comment on the use of `Definition d := Eval hnf in [expression]`
#28
gallais
opened
7 years ago
6
Chapter 5: typos + explanation on lambda-lifting + maximal insertion on Monoid.law
#27
gallais
closed
7 years ago
5
Chapter 4: typos + more details on the chain of coercions
#26
gallais
closed
7 years ago
1
Typos and mistakes
#25
sindikat
closed
7 years ago
4
Section on total functions + smaller changes
#24
ybertot
closed
7 years ago
4
Explain earlier how to turn an argument as implicit
#23
amahboubi
closed
5 years ago
0
Add a section about the totality of functions
#22
amahboubi
opened
7 years ago
2
§3.1.2, p. 81, footnote 2: a typo?
#21
anton-trunov
closed
7 years ago
1
§4.1.3: Lemma example uses andP view, which won't work with current definition of reflect
#20
anton-trunov
closed
5 years ago
1
Small fixes mainly for chapter 4
#19
anton-trunov
closed
7 years ago
1
Fix some typo
#18
MarisaKirisame
closed
7 years ago
3
§3.2.4: Line 3 in example "stamps" uses unexplained syntax
#17
darijgr
closed
5 years ago
3
update .gitignore
#16
anton-trunov
closed
7 years ago
0
Building instructions
#15
anton-trunov
opened
7 years ago
1
Improve tools for spellchecking
#14
amahboubi
opened
7 years ago
3
ch0: typo
#13
anton-trunov
closed
7 years ago
2
Common English language things
#12
mdnahas
closed
7 years ago
9
Added rudimentary spellchecking with aspell
#11
mdnahas
closed
7 years ago
3
various suggestions and corrections
#10
darijgr
closed
7 years ago
18
[ fix ] Fix a handful of typos in Chapter 2
#9
gallais
closed
7 years ago
1
Fix some typos in chapters 1, 2 & 3
#8
anton-trunov
closed
7 years ago
1
[ fix ] Fix a handful of typos in Chapter 1
#7
gallais
closed
7 years ago
1
The simplify_me lemma in sect 2.4 won't compile
#6
anton-trunov
closed
7 years ago
1
Example in chapter 2, sect. 2.3.3
#5
anton-trunov
closed
7 years ago
8
Previous
Next