Albert ten Napel atennapel

atennapel / infinitary-mutual-single-index.agda

Created January 5, 2022 15:36

Infinitary mutual inductive families signatures with a single index

	{-# OPTIONS --type-in-type #-}

	open import Agda.Builtin.Unit
	open import Agda.Builtin.Sigma
	open import Agda.Builtin.Equality
	open import Data.Product

	data IxCtx : Set where
	Nil : IxCtx
	Cons : Set -> IxCtx -> IxCtx

atennapel / SPropSketch.hs

Last active June 15, 2022 08:10

SProp sketch

	{-# LANGUAGE PatternSynonyms #-}
	{-# LANGUAGE OverloadedStrings #-}

	import Data.String (IsString(..))

	type Ix = Int
	type Lvl = Int
	type ULvl = Int

	data Sort = Type ULvl \| Prop

atennapel / anormalform.hs

Last active August 30, 2024 12:34

Normalization of polarized lambda calculus to A-normal form

	-- Polarized lambda calculus to A-normal form
	-- With eta-expansion and call-saturation

	type Ix = Int
	type Lvl = Int

	data Ty = TInt
	deriving (Show)
	data TFun = TFun [Ty] Ty
	deriving (Show)