From acef0f202be72e0281eaf79f1006f87c4d7e8916 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Thu, 25 Jun 2026 17:05:21 -0500 Subject: [PATCH] Add titles to documented modules Signed-off-by: Danila Fedorin --- lean/Spa/Interp.lean | 2 +- lean/Spa/Language/Base.lean | 2 +- lean/Spa/Language/Graphs.lean | 2 +- lean/Spa/Lattice.lean | 2 +- 4 files changed, 4 insertions(+), 4 deletions(-) diff --git a/lean/Spa/Interp.lean b/lean/Spa/Interp.lean index 62fb922..0123189 100644 --- a/lean/Spa/Interp.lean +++ b/lean/Spa/Interp.lean @@ -2,7 +2,7 @@ import Mathlib.Tactic.TypeStar /-! -Interpretation to a semantic domain. +# Interpretation to a Semantic Domain This file serves to introduce the double-angle-bracket "denotation" notation by prodiving a class instance `Interp`, whose single diff --git a/lean/Spa/Language/Base.lean b/lean/Spa/Language/Base.lean index 5fcdc72..8038004 100644 --- a/lean/Spa/Language/Base.lean +++ b/lean/Spa/Language/Base.lean @@ -2,7 +2,7 @@ import Mathlib.Data.Finset.Basic /-! -Base language. +# Base Language This file defines the core object language for the program analysis and transformation. It's a very basic imperative language. The `Spa/Language/Tagged/Basic.lean` diff --git a/lean/Spa/Language/Graphs.lean b/lean/Spa/Language/Graphs.lean index e10c535..59c5223 100644 --- a/lean/Spa/Language/Graphs.lean +++ b/lean/Spa/Language/Graphs.lean @@ -5,7 +5,7 @@ import Mathlib.Data.List.FinRange /-! -Algebraic Control Flow Graphs. +# Algebraic Control Flow Graphs This file defines control flow graphs and operations to naturally compose them, making it possible to inductively covnert a program in the object language diff --git a/lean/Spa/Lattice.lean b/lean/Spa/Lattice.lean index 5c59215..34cf3d7 100644 --- a/lean/Spa/Lattice.lean +++ b/lean/Spa/Lattice.lean @@ -3,7 +3,7 @@ import Mathlib.Order.RelSeries /-! -Lattice Definitions. +# Lattice Definitions This file provides some definitions for lattices. It used to be more critical when this was an Agda project, since it defined (semi)lattices, the ordering