| 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 |
| width = 20 | |
| height = 20 | |
| score = 0 | |
| import os | |
| import sys | |
| import tty | |
| import termios |
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.
| 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 |