From 4965c316c907c6d5ab273d1666b2ad5e9ab26f98 Mon Sep 17 00:00:00 2001 From: depsterr Date: Sun, 9 Oct 2022 01:11:34 +0200 Subject: [PATCH] fix CwF to be lagda --- src/CwF.lagda.md | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/src/CwF.lagda.md b/src/CwF.lagda.md index fc85340..4ec06a0 100644 --- a/src/CwF.lagda.md +++ b/src/CwF.lagda.md @@ -1,3 +1,7 @@ -module CwF where +``` +open import public CwF.Base -open import public CwF.Base \ No newline at end of file +module CwF where +``` + +This module just re-exports `CwF.Base`.