j jake-87

V2:

theory Isabelle_little_compiler
  imports Main
begin

datatype lang = 
  Lit nat
  | Plus lang lang

A somewhat brief overview of typechecking System F

This document comprises an example of typechecking a type system based on System F, in a small ML-like language.

You can skip the below section if you already understand System F itself.

System F is the name given to an extension of the simply typed lambda calclus.

	open import Relation.Binary.PropositionalEquality
	open import Data.Product
	open import Data.Bool
	open import Relation.Nullary.Negation
	open import Data.Sum
	open import Data.Empty

	postulate LEM : ∀ {ℓ} (A : Set ℓ) → A ⊎ (¬ A)
	postulate funext : ∀ {ℓ} {A B : Set ℓ} {f g : A → B} → (∀ x → f x ≡ g x) → f ≡ g

	{-# LANGUAGE StrictData, OverloadedStrings #-}
	{-# OPTIONS_GHC -Wall #-}
	{-# OPTIONS_GHC -Wno-unused-matches -Wno-unused-top-binds #-}
	{-# OPTIONS_GHC -Wno-unused-imports -Wno-name-shadowing #-}
	{-# LANGUAGE PartialTypeSignatures #-}
	import Data.STRef
	import Control.Monad.ST
	import Text.Show.Functions
	import Control.Monad.Except
	import Control.Monad.Trans.Class

	open import Relation.Binary.PropositionalEquality
	open import Data.Nat
	open import Data.Nat.Properties
	open import Data.Maybe
	open import Data.Fin
	open import Relation.Nullary.Decidable
	open import Data.Product

	data Con : ℕ → Set
	data Tm : ℕ → Set

	Copyright <YEAR> <COPYRIGHT HOLDER>

	Redistribution and use in source and binary forms, with or without modification, are permitted provided that
	the following conditions are met:

	1. Redistributions of source code must retain the above copyright notice, this list of conditions and the
	following disclaimer.

	2. Redistributions in binary form are permitted only under the following conditions:

	sudo apt install build-essential texinfo
	sudo dpkg-reconfigure dash
	sudo mkdir /mnt/lfs
	echo "What partition should be mounted for LFS?"
	read -p "Path : " mntpath
	sudo mount $mntpath /mnt/lfs
	export LFS=/mnt/lfs