Jesper

Belgium

top accounts reputation activity subscriptions

How to use of laziness in Scheme efficiently?

performance scheme lazy-evaluation asked Dec 27, 2021 at 23:16

stackoverflow.com

7 votes

What was the first proof assistant with eta equality for records?

coq agda eta-equality records asked Dec 21, 2022 at 14:51

proofassistants.stackexchange.com

6 votes

Is this battlemaster houserule balanced?

dnd-5e house-rules balance fighter asked Aug 24, 2015 at 15:55

rpg.stackexchange.com

6 votes

How to scale up exploration challenges to mid and high levels?

dnd-5e gm-preparation exploration asked Jul 22, 2020 at 6:53

rpg.stackexchange.com

Top Answers

What is Axiom K?

stackoverflow.com

What else can you do in the turn you ready an action?

rpg.stackexchange.com

Is it possible to get hold of free theorems as propositional equalities?

stackoverflow.com

Why we cannot pattern match on Set/Type in Coq/Agda/Idris？

stackoverflow.com

What subtyping rules does Agda support?

proofassistants.stackexchange.com

Termination and confluence -- which goes first?

proofassistants.stackexchange.com

What is positivity checking?

stackoverflow.com

Small kernel (i.e. proof-verifier) for Agda?

cstheory.stackexchange.com

How to use Prop from UTT in Agda

stackoverflow.com

Why does Agda give error "expected: ℕ, actual: ℕ"

stackoverflow.com

What's the effect of imposing the following restriction on inductive type families?

cstheory.stackexchange.com

Equality testing without explicit proof that data constructors are injective

stackoverflow.com

What does errors like "!=<" mean in agda and how to fix

stackoverflow.com

Agda records: field alias

stackoverflow.com

Convert indexed Agda data type to record

stackoverflow.com

Unresolved metas in for run in Agda hello-world

stackoverflow.com

Why does Agda require pattern matching here

stackoverflow.com

What is the state of recompilation avoidance in proof assistants?

proofassistants.stackexchange.com