Skip to content

Commit

Permalink
feat: function to run experiments plainly
Browse files Browse the repository at this point in the history
without drawing boxes around them and other fancy stuff
  • Loading branch information
pmbittner committed Sep 25, 2024
1 parent 7e56aaa commit 7c98c9e
Showing 1 changed file with 7 additions and 0 deletions.
7 changes: 7 additions & 0 deletions src/Vatras/Test/Experiment.agda
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down

0 comments on commit 7c98c9e

Please sign in to comment.