Well it is a subset of F\* which compiles to C. So you do not compile to lowstar...

		tluyben2 on Aug 17, 2020 \| parent \| context \| favorite \| on: Idris 2 version 0.2.1 Well it is a subset of F* which compiles to C. So you do not compile to lowstar, lowstar is the F* you write which compiles to C.