JakobBruenker

{-# LANGUAGE TypeFamilies, UndecidableInstances, KindSignatures, DataKinds, TypeOperators, GADTs, RankNTypes, PolyKinds #-}

import Data.Kind
import Data.Type.Equality

data Nat = Z | S Nat

data SNat :: Nat -> Type where
  SZ :: SNat Z
  SS :: SNat n -> SNat (S n)

JakobBruenker

{-# LANGUAGE DataKinds
           , ScopedTypeVariables
           , TypeApplications
           , TypeFamilies
           , PolyKinds
           , StandaloneKindSignatures
           #-}

module MaybeBug where

JakobBruenker

{-# LANGUAGE GADTs
           , KindSignatures
           , DataKinds
           , PolyKinds
           , TypeFamilies
           #-}

import GHC.TypeLits hiding (Nat)

-- | Store a dict saying that one symbol is smaller than another

JakobBruenker

import java.util.function.Function;

// This is only actually a proof of anything if you assume that null doesn't
// exist, and that all functions are pure and terminate
public class WeakDNE {
    // False has no values
    public static final class False {
        private final Absurd absurdFun;

        // Helper interface to encode rank 2 type

JakobBruenker

module Minimal where

open import Agda.Builtin.Nat renaming (Nat to ℕ)
open import Agda.Primitive
open import Agda.Builtin.Bool
open import Agda.Builtin.Equality
open import Agda.Builtin.Sigma

infixr 2 _×_

JakobBruenker

module Combinators where

open import Agda.Builtin.Nat renaming (Nat to ℕ)
open import Agda.Primitive
open import Agda.Builtin.Bool
open import Agda.Builtin.Equality
open import Agda.Builtin.Sigma
  renaming (fst to proj₁; snd to proj₂)
    hiding (module Σ)
module Σ = Agda.Builtin.Sigma.Σ

JakobBruenker

open import Agda.Builtin.Sigma
open import Agda.Builtin.Equality

lemma : ∀ {a b} {A : Set a} {B : A → Set b} {x x' : A} {p p' : B}
      → (x , p) ≡ (x' , p') → ((x ≡ x') , (p ≡ p'))
lemma = ?

{-
Checking Test (/home/user/agda/combinators/Test.agda).
/home/user/agda/combinators/Test.agda:4,64-65

JakobBruenker

module TooLong where

open import Agda.Builtin.Nat renaming (Nat to ℕ)
open import Agda.Primitive
open import Agda.Builtin.Bool
open import Agda.Builtin.Equality

data SK : Set where
  S : SK
  K : SK

JakobBruenker

{-# OPTIONS_GHC -Wall -Wno-unticked-promoted-constructors #-}
{-# LANGUAGE Haskell2010
  , TypeFamilies
  , DataKinds
  , PolyKinds
  , RankNTypes
  , TypeOperators
  , TemplateHaskell
  , GADTs
  , ScopedTypeVariables

JakobBruenker

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE EmptyCase #-}