Skip to main content

Questions tagged [pie]

Questions related to Pie, the dependently typed companion language to "The Little Typer"

Filter by
Sorted by
Tagged with
4 votes
2 answers
661 views

In a dependently typed language, are all types statements?

In dependently typed languages such as Agda, Lean, Coq, Idris (and Pie), a mathematical or logical statement can be expressed as a type, and then proven by writing a program that creates an instance ...
Mars's user avatar
  • 141
1 vote
2 answers
254 views

Is it possible to prove (-> (= (Either Trivial Trivial) (left sole) (right sole)) Absurd) in Pie?

In this question, I am talking about the language Pie described in the book The Little Typer. One can derive that $0=1$ is contradictory: ...
CrabMan's user avatar
  • 317
1 vote
1 answer
100 views

Why is the normal form of an ind-Nat expression with a function type an elimination-of-a-function expression

In this question, I am talking about the language Pie described in the book The Little Typer. Consider the definition ...
CrabMan's user avatar
  • 317