search

idris-lang / Idris2

A purely functional programming language with first class types
https://idris-lang.org/
Other
2.46k stars 369 forks source link

Nested code blocks are ignored in literate markdown #3342

Open joelberkeley opened 2 days ago

joelberkeley commented 2 days ago

Steps to Reproduce

Type check the following markdown

```idris
x : Nat
x = ""

Expected Behavior

Both code blocks fail type-checking

Observed Behavior

Only the first fails