From 42fe6fb304b322b2bfabab243964375520f46973 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Fri, 9 Feb 2024 15:24:57 +0100 Subject: Add some demo files --- tests/lean/lakefile.lean | 1 + 1 file changed, 1 insertion(+) (limited to 'tests/lean/lakefile.lean') diff --git a/tests/lean/lakefile.lean b/tests/lean/lakefile.lean index 781fc8b8..3a777824 100644 --- a/tests/lean/lakefile.lean +++ b/tests/lean/lakefile.lean @@ -20,3 +20,4 @@ package «tests» {} @[default_target] lean_lib PoloniusList @[default_target] lean_lib Arrays @[default_target] lean_lib Traits +@[default_target] lean_lib Demo -- cgit v1.2.3