From 7c98c9ec1a2854c9906a9e145a5912ab0e930dd6 Mon Sep 17 00:00:00 2001 From: pmbittner Date: Wed, 25 Sep 2024 18:03:25 +0200 Subject: [PATCH] feat: function to run experiments plainly without drawing boxes around them and other fancy stuff --- src/Vatras/Test/Experiment.agda | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/src/Vatras/Test/Experiment.agda b/src/Vatras/Test/Experiment.agda index 1c487bb4..d8cb0040 100644 --- a/src/Vatras/Test/Experiment.agda +++ b/src/Vatras/Test/Experiment.agda @@ -31,6 +31,13 @@ ExperimentSetup ℓ = Σ[ A ∈ Set ℓ ] (Experiment A × List (Example A)) setup : ∀ {ℓ} {A : Set ℓ} → Experiment A → List (Example A) → ExperimentSetup ℓ setup {ℓ} {A} program inputs = A , program , inputs +run-experiment-plain : ∀ {ℓ} {A : Set ℓ} → Experiment A → Example A → Lines +run-experiment-plain experiment example = do + > "Run Experiment " ++ getName experiment ++ " on " ++ getName example + linebreak + get experiment example + linebreak + run-experiment : ∀ {ℓ} {A : Set ℓ} → Experiment A → Example A → Lines run-experiment experiment example = do linebreak