shhyou

#lang racket/base

(require racket/list
         racket/vector
         racket/bytes
         racket/match)

(provide
 ;; plain implementation of the Burrows-Wheeler transformation
 (struct-out bwencode)

shhyou

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

-- using an inductive datatype (family) instead of El

module MutualRecData where

open import Agda.Primitive

open import Data.Nat.Base
  using (ℕ ; zero ; suc)

shhyou

#lang racket/gui
(require plot
         pict)

;;; Author: Laurent Orseau
;;; License: [Apache License, Version 2.0](http://www.apache.org/licenses/LICENSE-2.0) or
;;;          [MIT license](http://opensource.org/licenses/MIT) at your option.

;;; See in particular this blog bost:
;;; https://alex-hhh.github.io/2019/09/map-snip.html#2019-09-08-map-snip-footnote-2-return

shhyou

[
  {
      "key": "ctrl+shift+tab",
      "command": "workbench.action.previousEditor"
  },
  {
      "key": "ctrl+tab",
      "command": "workbench.action.nextEditor"
  }
]

shhyou

{-# OPTIONS --safe #-}

module ULCOmega where

open import Data.Nat.Base using (ℕ ; zero ; suc)
open import Data.Fin.Base as Fin using (Fin)

import Data.Nat.Literals
import Data.Fin.Literals
open import Data.Unit using (⊤ ; tt) -- for instance resolution

shhyou

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

module TwistedMaxAcc where

open import Data.Nat using (ℕ ; zero ; suc ; _>_ ; _≤_ ; _≤″_ ; less-than-or-equal ; _≰_ ; _>?_ ; _≤?_ ; _+_)
open import Data.Nat.Properties using (≤-reflexive ; ≤-antisym ; ≮⇒≥ ; >⇒≢ ; ≤⇒≤″ ; m≤m+n ; +-suc ; +-comm)
open import Data.Empty using (⊥-elim ; ⊥)
open import Relation.Nullary using (Dec ; yes ; no)
open import Relation.Binary.PropositionalEquality.Core using (refl ; _≡_ ; subst ; sym)

shhyou

#|
building syntax objects
cpu time: 106 real time: 112 gc time: 45
expanding
cpu time: 16063 real time: 17360 gc time: 2152

building syntax objects 2
cpu time: 116 real time: 126 gc time: 50
expanding
cpu time: 15898 real time: 16583 gc time: 2231

shhyou

{- Coquand, T., & Dybjer, P. (1997). Intuitionistic model constructions and normalization proofs.
  Mathematical Structures in Computer Science, 7(1). https://doi.org/10.1017/S0960129596002150 -}

open import Data.Empty                            using (⊥)
open import Data.Unit                             using (⊤; tt)
open import Data.Nat                              using (ℕ; zero; suc)
open import Data.Product                          using (_×_; _,_; Σ; proj₁; proj₂; ∃-syntax)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans; cong)

infix 3 _-→_ _-↛_

shhyou

{-# OPTIONS --without-K --safe #-}
{- Works with Agda 2.6.2 -}

module InstMagic where

open import Relation.Binary.PropositionalEquality using ( _≡_ ; refl)
open import Data.List using (List ; [] ; _∷_)
open import Data.Unit using (⊤ ; tt)
open import Data.Nat using (ℕ ; zero ; suc ; _≟_)
open import Data.List.Relation.Unary.Any using (Any ; any? ; here ; there)

shhyou

#lang racket/base

(require racket/list
         racket/match
         racket/class
         racket/pretty
         racket/snip
         racket/gui/base
         framework)