Stack Exchange

gallais

Dundee, Scotland, UK

http://gallais.github.io

top accounts reputation activity subscriptions
Top Questions
Top Answers
24
How do I verify the Coq proof of Feit-Thompson?
mathoverflow.net

20
Why should you "never resort to polymorphism when initiality would do"?
proofassistants.stackexchange.com

17
Open Type Level Proofs in Haskell/Idris
stackoverflow.com

17
How to switch the current goal in Coq?
stackoverflow.com

16
Coq execution difference between semicolon ";" and period "."
stackoverflow.com

14
Why does Coq have Prop?
cstheory.stackexchange.com

14
How can I rewrite "+ 1" (plus one) to "S" (succ) in Coq?
stackoverflow.com

14
What does an apostrophe in front of a list ( '[Something] ) mean in Haskell?
stackoverflow.com

13
Is it possible to use church encodings without breaking equational reasoning?
stackoverflow.com

12
Proof assistant for mathematics only
stackoverflow.com

12
What should I do if two modules share the same name?
stackoverflow.com

11
List based on right Kan extension
stackoverflow.com

11
Can a type system serve as a proof assistant for foreign functions?
cs.stackexchange.com

11
"Minimal" intuitionistic type theory?
cs.stackexchange.com

11
How to map Type to Value in Idris/Agda/Coq?
stackoverflow.com

10
Coq: keeping information in a match statement
stackoverflow.com

10
Is it possible to evaluate lambda calculus terms efficiently?
stackoverflow.com

10
Type theory and computational complexity
cstheory.stackexchange.com

10
Could not deduce KnownNat in two existentials with respect to the singletons library
stackoverflow.com

9
What is the correct definition of `unfold` for an untagged tree?
stackoverflow.com

9
Idris non-trivial type computation for tensor indexing
stackoverflow.com

8
How to define abstract types in agda
stackoverflow.com

8
How do I refer to the same type variable in different type annotations?
stackoverflow.com

8
Proving uniqueness of an instance of an indexed inductive type
proofassistants.stackexchange.com

8
How to disable my custom notation in Coq?
stackoverflow.com

8
Constructive proof of strong normalization for simply typed lambda calculus
proofassistants.stackexchange.com

8
Coq proof that type isomorphism relationship is transitive
codereview.stackexchange.com

8
Is it possible to write a non-terminating web server in agda?
stackoverflow.com

8
Coq simpl for Program Fixpoint
stackoverflow.com

7
How to prove f x < f y → x ≢ y
proofassistants.stackexchange.com

1 2 3