No questions with score of 5 or more
How do I verify the Coq proof of Feit-Thompson?
Is it possible to use church encodings without breaking equational reasoning?
Open Type Level Proofs in Haskell/Idris
List based on right Kan extension
How do I refer to the same type variable in different type annotations?
Why does Coq have Prop?
Proof assistant for mathematics only
Might laziness also mean a value of function depends on context where it is called?
How to define abstract types in agda
Type hierarchy definition in Coq or Agda
What is the correct definition of `unfold` for an untagged tree?
Order of operations - why are they in the order they're in?
Coq: keeping information in a match statement
Is it possible to evaluate lambda calculus terms efficiently?
Define an inductive dependent-type with constraints on the type-parameter
Translation from basic While-language to $\lambda$-calculus
Function to Map `[a] -> [[a]]`