From 3ea12fef67c58dfdb70ef23404e36bdfa62aff73 Mon Sep 17 00:00:00 2001 From: rhiannon morris Date: Mon, 7 Mar 2022 01:19:26 +0100 Subject: [PATCH] important feature: banner --- src/Quox.idr | 14 +++++++++++++- 1 file changed, 13 insertions(+), 1 deletion(-) diff --git a/src/Quox.idr b/src/Quox.idr index 7deaaf3..8045498 100644 --- a/src/Quox.idr +++ b/src/Quox.idr @@ -11,6 +11,18 @@ import Data.Nat import Data.Vect +export +banner : String +banner = #""" + _ ___,-´/ + (.`--´ ∪ -´/ ___ ___ _____ __ __ + \/\/--´`´`--´ / _ `/ // / _ \\ \ / + U ---, / \_, /\_,_/\___/_\_\ + /--/ | /_/ + /--/ | + + """# + export tm : Term 1 2 tm = @@ -20,6 +32,6 @@ tm = main : IO Unit main = do + putStrLn banner prettyTerm tm prettyTerm $ pushSubstsT tm - putStrLn "\n:qtuwu:"