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

useronym

open import Data.Nat
open import Data.Bool

mutual
  data Stream (A : Set) : Set where
    []ˢ : Stream A
    _∷ˢ_ : A → ∞Stream A → Stream A

  record ∞Stream (A : Set) : Set where
    coinductive

L-TChen

{-# LANGUAGE FlexibleContexts, FlexibleInstances #-}
{-# LANGUAGE TypeInType , ScopedTypeVariables , TypeFamilies, TypeOperators #-} 
{-# LANGUAGE GADTs, StandaloneDeriving #-}
{-# LANGUAGE Safe #-}

module Unification where

import Data.Kind
import Prelude hiding ((++))