roconnor

(* This Normalization by Evaluation is based on mietek's <https://research.mietek.io/A201801.FullIPLNormalisation.html>.
   I've removed the continuations to give a purely tree-based implementation.
   This is operationally less efficent than using continuations, but it is hopefully easier to understand and potentially easier to verify correct.

   Checked with Coq 8.18.0
*)

Inductive Form :=
| Zero : Form
| One : Form

TOTBWF

{-# OPTIONS --without-K --safe #-}

open import Categories.Category.Core
open import Categories.Category.Cartesian

module Categories.Tactic.Cartesian.Solver {o ℓ e} {𝒞 : Category o ℓ e} (cartesian : Cartesian 𝒞) where

open import Level

open import Categories.Category.BinaryProducts

andrejbauer

open import Level
open import Relation.Binary
open import Data.Product
open import Data.Unit
open import Agda.Builtin.Sigma
open import Relation.Binary.PropositionalEquality renaming (refl to ≡-refl; trans to ≡-trans; sym to ≡-sym; cong to ≡-cong)
open import Relation.Binary.PropositionalEquality.Properties
open import Function.Equality hiding (setoid)

module Epimorphism where

wenkokke

Tactics in Agda

This gist is my attempt to list all projects providing proof automation for Agda.

Glossary

When I say tactic, I mean something that uses Agda's reflection to provide a smooth user experience, such as the solveZ3 tactic from Schmitty:

_ : ∀ (x y : ℤ) → x ≤ y → y ≤ x → x ≡ y
_ = solveZ3

andrejbauer

open import Data.Nat
open import Data.Fin as Fin

module Primrec where

  -- The datatype of primitive recursive function
  data PR : ∀ (k : ℕ) → Set where
    pr-zero : PR 0 -- zero
    pr-succ : PR 1 -- successor
    pr-proj : ∀ {k} (i : Fin k) → PR k -- projection

AndrasKovacs

{-# language Strict, BangPatterns, LambdaCase, ViewPatterns, OverloadedStrings #-}
{-# options_ghc -Wincomplete-patterns #-}

-- NbE with case commutation for sum types.

import Data.Maybe
import Data.String

type Name = String

bobatkey

{-# OPTIONS --rewriting #-}

module cont-cwf where

open import Agda.Builtin.Sigma
open import Agda.Builtin.Unit
open import Agda.Builtin.Bool
open import Agda.Builtin.Nat
open import Data.Empty
import Relation.Binary.PropositionalEquality as Eq

AndrasKovacs

{-
Inductive-recursive universes, indexed by levels which are below an arbitrary type-theoretic ordinal number (see HoTT book 10.3). This includes all kinds of transfinite levels as well.

Checked with: Agda 2.6.1, stdlib 1.3

My original motivation was to give inductive-recursive (or equivalently: large inductive)
semantics to to Jon Sterling's cumulative algebraic TT paper:

Blaisorblade

{-# OPTIONS --type-in-type --no-positivity-check  #-}

module InconsistentImpredicativeSums where
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary
open import Relation.Nullary.Negation
open import Data.Product
open import Data.Empty
-- hiding (⊥-elim)
-- open import Data.Empty.Irrelevant

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