Pinned

1. Normalization by evaluation for Syst...

   1

   {- Coquand, T., & Dybjer, P. (1997). Intuitionistic model constructions and normalization proofs.

   2

     Mathematical Structures in Computer Science, 7(1). https://doi.org/10.1017/S0960129596002150 -}

   3

   4

   open import Data.Empty                            using (⊥)

   5

   open import Data.Unit                             using (⊤; tt)

2. An implementation of McBride's struc...

   1

   {-# LANGUAGE FlexibleContexts, FlexibleInstances #-}

   2

   {-# LANGUAGE TypeInType , ScopedTypeVariables , TypeFamilies, TypeOperators #-} 

   3

   {-# LANGUAGE GADTs, StandaloneDeriving #-}

   4

   {-# LANGUAGE Safe #-}

   5

3. FiniteSets Public

   Fintie Sets in Cubical Agda

   Agda 12

4. MtacAR Public

   Mtac in Agda

   Agda 29