From 992aa8fdd40521d2cc7ed4759bce92c912cbeb80 Mon Sep 17 00:00:00 2001 From: Hannes Schulze Date: Mon, 20 Oct 2025 13:13:33 +0200 Subject: further work --- Nominal.lean | 1 + 1 file changed, 1 insertion(+) (limited to 'Nominal.lean') diff --git a/Nominal.lean b/Nominal.lean index a3f0848..c94bb05 100644 --- a/Nominal.lean +++ b/Nominal.lean @@ -1,3 +1,4 @@ -- This module serves as the root of the `Nominal` library. -- Import modules here that should be built as part of the library. +import Nominal.Permutations import Nominal.Basic -- cgit v1.3.1