The compactness theorem for countable models is equivalent to the weak König's lemma by a result of H. Friedman and others as noted [here](http://mathoverflow.net/questions/228389), in the context of classical logic. The weak König's lemma in constructive mathematics has been extensively studied as noted [here](http://mathoverflow.net/questions/228468). What is the status of the *compactness theorem for countable models* itself in constructive mathematics?

Note 1. One relevant paper seems to be *Moerdijk, Ieke; Palmgren, Erik. Minimal models of Heyting arithmetic. J. Symbolic Logic  62  (1997),  no. 4, 1448–1460.*