Questions tagged [pie]

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

Filter by
Sorted by
Tagged with
1 vote
2 answers
233 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: ...
  • 317
1 vote
1 answer
84 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 ...
  • 317