diff options
| author | adelon <22380201+adelon@users.noreply.github.com> | 2025-12-16 17:10:31 +0100 |
|---|---|---|
| committer | adelon <22380201+adelon@users.noreply.github.com> | 2025-12-16 17:10:31 +0100 |
| commit | ed546f3ce3d7c4e5840387beb2d89c8da05378ea (patch) | |
| tree | 8eab7129b4eea05159af7e820b4631897299bce5 /source/Megalodon.hs | |
| parent | 8e7d2c94d8449b8512fd6257534b4c593319b4ae (diff) | |
Add location info to implicit QED step
Diffstat (limited to 'source/Megalodon.hs')
| -rw-r--r-- | source/Megalodon.hs | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/source/Megalodon.hs b/source/Megalodon.hs index 295ab15..e7dfeb5 100644 --- a/source/Megalodon.hs +++ b/source/Megalodon.hs @@ -30,7 +30,7 @@ buildBlocks lexi = \case BlockAxiom _pos lbl (Axiom asms stmt) : blocks -> let phi = closure (unAsm <$> asms) stmt in text "Fact " <> buildMarker lbl <> text " : " <> buildFormula lexi phi <> text ".\nAdmitted.\n" <> buildBlocks lexi blocks - BlockLemma _pos lbl (Lemma asms stmt) : BlockProof _ _ : blocks -> + BlockLemma _pos lbl (Lemma asms stmt) : BlockProof _ _ _ : blocks -> let phi = closure (unAsm <$> asms) stmt in text "Theorem " <> buildMarker lbl <> text " : " <> buildFormula lexi phi <> text ".\nAdmitted.\n" <> buildBlocks lexi blocks BlockLemma _pos lbl (Lemma asms stmt) : blocks -> |