Tour
About Us
Meta
Loading…
Log in
current community
Stack Exchange
chat
Meta Stack Exchange
your communities
Sign up
or
log in
to customize your list.
more stack exchange communities
company blog
Stack Exchange
All Sites
Top Users
Digests
gallais
Glasgow, Scotland
http://www.gallais.org
top
accounts
reputation
activity
bookmarks
subscriptions
Top Questions
7
votes
Application of type-level arguments of Kind other than Type
haskell
type-kinds
asked Oct 13 '17 at 10:13
stackoverflow.com
7
votes
Implicit arguments in a computed type in Coq
types
coq
asked Nov 9 '17 at 11:02
stackoverflow.com
6
votes
Checking that two values have the same head constructor
haskell
asked May 12 '17 at 18:10
stackoverflow.com
5
votes
ghc does not report non-exhaustive pattern matches when using the `no-code` flag
haskell
pattern-matching
typechecking
asked Dec 25 '14 at 12:47
stackoverflow.com
5
votes
Memoizing an effectful function
haskell
memoization
unsafe-perform-io
asked Sep 11 '15 at 14:33
stackoverflow.com
Top Answers
23
How do I verify the Coq proof of Feit-Thompson?
mathoverflow.net
18
How to switch the current goal in Coq?
stackoverflow.com
17
Open Type Level Proofs in Haskell/Idris
stackoverflow.com
16
Coq execution difference between semicolon “;” and period “.”
stackoverflow.com
14
Why does Coq have Prop?
cstheory.stackexchange.com
13
Is it possible to use church encodings without breaking equational reasoning?
stackoverflow.com
13
How can I rewrite “+ 1” (plus one) to “S” (succ) in Coq?
stackoverflow.com
11
List based on right Kan extension
stackoverflow.com
11
Proof assistant for mathematics only
stackoverflow.com
11
What should I do if two modules share the same name?
stackoverflow.com
11
What does an apostrophe in front of a list ( '[Something] ) mean in Haskell?
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
10
Is it possible to evaluate lambda calculus terms efficiently?
stackoverflow.com
10
Type theory and computational complexity
cstheory.stackexchange.com
10
How to map Type to Value in Idris/Agda/Coq?
stackoverflow.com
10
Could not deduce KnownNat in two existentials with respect to the singletons library
stackoverflow.com
8
Coq proof that type isomorphism relationship is transitive
codereview.stackexchange.com
8
How do I refer to the same type variable in different type annotations?
stackoverflow.com
8
Coq: keeping information in a match statement
stackoverflow.com
8
What is the correct definition of `unfold` for an untagged tree?
stackoverflow.com
8
Idris non-trivial type computation for tensor indexing
stackoverflow.com
7
How to handle sums in Tait's reducibility proof of strong normalisation?
mathoverflow.net
7
Casting a nullary data constructor between types
softwareengineering.stackexchange.com
7
Type Level Fix Point while Ensuring Termination
stackoverflow.com
7
Haskell: How is Num held?
stackoverflow.com
7
Why are ML/Haskell datatypes useful for defining “languages” like arithmetic expressions?
stackoverflow.com
7
Proving a sorting operation in type system
cs.stackexchange.com
7
How to define abstract types in agda
stackoverflow.com
7
Coq simpl for Program Fixpoint
stackoverflow.com
1
2
3
next
Stack Exchange works best with JavaScript enabled