LAC – Lean lecture material (COMP2012)

This repository contains the lecture and exercise material for COMP2012 (Languages and Computation), using Lean 4 with mathlib.

The material is organised as a Lake project and updated regularly during the semester.

Repository structure

Lectures/ lecture files used in class
Exercises/ exercise sheets
Proofs/ Lean code from the lecture notes

All Lean imports start with LAC, for example:

import LAC.Proofs.Lang

Name		Name	Last commit message	Last commit date
Latest commit History 22 Commits
Exercises		Exercises
Lectures		Lectures
Proofs		Proofs
.gitignore		.gitignore
Lectures.lean		Lectures.lean
README.md		README.md
lake-manifest.json		lake-manifest.json
lakefile.toml		lakefile.toml
lean-toolchain		lean-toolchain
publish.sh		publish.sh