User Andrej Bauer - Proof Assistants Stack Exchange

Andrej Bauer

Member for 1 year, 9 months
Last seen this week

andrej.com
Ljubljana

101 Answers

Score Activity Newest

2 votes

Accepted

How do you implement what's in the Pierce Book precisely? And why / why not have evaluation just mutate ParseTree's of a PEG parser generator library?

answered Oct 30, 2022 at 8:42

2 votes

Natural deduction vs simply typed lambda calculus

answered Jul 9, 2022 at 19:14

1 vote

Can you remove strict positivity from mere propositions?

answered Jun 9, 2022 at 15:48

1 vote

What is a non-canonical term?

answered May 31, 2022 at 20:34

1 vote

Coq produce instance of a type `{x : T | P x}` inside an explicit definition given an `x'` of type `T`

answered Feb 28, 2022 at 12:07

1 vote

confused about stlc from Programming Language Foundations

answered Sep 6 at 19:02

1 vote

How do I extract efficient string code in Coq to OCaml?

answered Jul 15 at 9:05

1 vote

Inspecting proof terms in Agda

answered Jun 15 at 21:33

0 votes

Accepted

Existential quantification on types in Isabelle

answered Jul 3 at 19:20

0 votes

How do I define a function in Coq with if...then..else behavior?

answered Jan 8 at 10:32

0 votes

How do I express a fixpoint of a decreasing argument that is not a subterm of the function's argument?

answered Feb 2 at 18:05

4