User Mike Shulman

24 votes

0 answers

587 views

Categorical semantics of Agda

asked Dec 11, 2022 at 9:58

14 votes

2 answers

577 views

Tutorial implementations of NbE

asked Mar 16, 2022 at 18:00

12 votes

0 answers

175 views

Rules for mutual inductive/coinductive types

asked Mar 6, 2022 at 20:57

11 votes

1 answer

262 views

Universe inconsistency as an effect

asked Dec 16, 2022 at 20:37

11 votes

5 answers

2k views

How do real-world proof assistants bind variables and check equality?

asked Jun 3 at 1:57

10 votes

2 answers

195 views

Uses of first-class implicit function types

asked Dec 5, 2022 at 0:47

9 votes

1 answer

340 views

Strong eta-rules for functions on sum types

asked Dec 10, 2022 at 6:24

9 votes

2 answers

269 views

Notation for indefinite integrals

asked Feb 25, 2022 at 19:59

7 votes

1 answer

462 views

Very dependent functions

asked Sep 14, 2022 at 18:11

5 votes

2 answers

132 views

Comparing indexed induction to recursion

asked Feb 4 at 1:23

4 votes

2 answers

217 views

Binding variables to terms involving later variables

asked Feb 29 at 7:49

2 votes

1 answer

139 views

How to implement separate compilation?

asked Jun 15 at 6:03

Stack Exchange Network

12 Questions

Categorical semantics of Agda

Tutorial implementations of NbE

Rules for mutual inductive/coinductive types

Universe inconsistency as an effect

How do real-world proof assistants bind variables and check equality?

Uses of first-class implicit function types

Strong eta-rules for functions on sum types

Notation for indefinite integrals

Very dependent functions

Comparing indexed induction to recursion

Binding variables to terms involving later variables

How to implement separate compilation?