jespercockx

How to formalize stuff in Agda
==============================

Preliminaries
-------------

For this presentation, we keep the dependencies to a minimum.

```

jespercockx

{-# OPTIONS --without-K --rewriting --prop #-}

open import Agda.Primitive
open import Agda.Builtin.Nat
open import Agda.Builtin.Equality

variable
  ℓ : Level
  A B C : Set ℓ
  x y z : A

jespercockx

Without covering clauses
-----------------------------------------

512K	./src/Algebra.agdai
28K	./src/Debug/Trace.agdai
72K	./src/Record.agdai
52K	./src/Function.agdai
20K	./src/Strict.agdai
64K	./src/Induction/Lexicographic.agdai
24K	./src/Induction/Nat.agdai

jespercockx

{-# OPTIONS --guardedness #-}

open import Agda.Builtin.Unit
open import Agda.Builtin.Size

record _×_ (A B : Set) : Set where
  constructor _,_
  field
    fst : A
    snd : B

jespercockx

{-
======================================
=== THE GREAT RESURRECTION OF PROP ===
======================================

Bringing back the impredicative sort Prop of definitionally proof-irrelevant propositions to Agda.

To check this file, get the prop-rezz branch of Agda at https://github.com/jespercockx/agda/tree/prop-rezz.

This file is a short demo meant to show what you currently can (and can't) do with Prop.

jespercockx

diff --git a/src/Bool.agda b/src/Bool.agda
index 25a0a7f..ff7c092 100644
--- a/src/Bool.agda
+++ b/src/Bool.agda
@@ -86,7 +86,7 @@ not≡↔≡not {false} {false} =
 
 -- Some lemmas related to T.
 
-T↔≡true : ∀ {b} → T b ↔ b ≡ true
+T↔≡true : {b : Bool} → T b ↔ b ≡ true