jake-87

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

jake-87

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:

jake-87

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.

A brief overview of System F

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

jake-87

width = 20
height = 20

score = 0

import os
import sys
import tty
import termios

jake-87

jake-87

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

jake-87

let rand =
  let x = ref 10 in
  fun () ->
  x := (!x * 27527 + 27791) mod 41231;
  !x

type tree =
  | Leaf
  | Branch of int * tree * tree

jake-87

{-# 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

jake-87

V2:

theory Isabelle_little_compiler
  imports Main
begin

datatype lang = 
  Lit nat
  | Plus lang lang

jake-87

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