Skip to main content
ejgallego's user avatar
ejgallego's user avatar
ejgallego's user avatar
ejgallego
Co-Applicative
  • Member for 11 years, 6 months
  • Last seen this week
  • Paris, France
Profile Activity
Stats
6,812
reputation
117k
reached
197
answers
5
questions
Communities
View all
About

Computer Scientist, Programmer, Musician.

Golden rule for Coq Programming: If you start to feel lots of pain in your proofs, you are likely doing it wrong!

Badges
View all badges
1
gold badge
15
silver badges
30
bronze badges
Top tags
View all tags
530
Score
196
Posts
97
Posts %
93
Score
38
Posts
19
Posts %
52
Score
18
Posts
9
Posts %
21
Score
6
Posts
3
Posts %
16
Score
7
Posts
3
Posts %
14
Score
8
Posts
4
Posts %
Top posts
View all questions, answers, and articles
19
How to define set in coq without defining set as a list of elements
Apr 13, 2016
16
How to call proof asistant Coq from external software
Sep 4, 2017
10
How is Coq's parser implemented?
Apr 4, 2017
9
what does the colon greater than sign mean in coq
Dec 16, 2016
9
Why would the tactic 'exact' be complete for Coq proofs?
Sep 24, 2017
7
Does ssreflect assume excluded middle?
Jan 28, 2016
7
Coq eapply generates a goal with a question mark while proving existence of a function
Jan 9, 2017
7
How is a .vo file structured so that coqchk may use it?
Feb 18, 2018
7
Coq: destruct (co)inductive hypothesis without losing information
Jul 17, 2017
7
Using destruct on pattern match expression with 'convoy pattern'
Nov 17, 2017
Top network posts
View all network posts
9
Chainload from windows boot manager to Grub with Secure Boot enabled
5
Proof of equality with destructuring let...in