TK
В общем, не зря есть неполные по Тьюрингу япы
Size: a a a
2021 May 26
TK
Но пускай в своей нише остаются
ΑZ
use envconfig::Envconfig;
pub struct DotenvProof(());
pub fn dotenv_with_proof() -> Result<DotenvProof, dotenv::Error> {
dotenv::dotenv().map(|_| DotenvProof(()))
}
Вот например. У меня тут по программе таскается пруф что мы зарузили энвы из файликаB
который ансейф?
ΑZ
ну да, как обычно же
TK
*smug face*
ΑZ
функции которым нужен энвайронмент требуют его в аргументах:
impl EnvConfig {
pub fn new(_: &DotenvProof) -> Result<Self, envconfig::Error> {
Self::init()
}
}B
ой, теперь сделаю макро мамайклянус!, утф8 иденты же завезли
ΑZ
и в целом работает
ΑZ
ну да, есть некий ансейф кор блок, что поделать
ΑZ
в идрисе на практике он тоже будет, потому что доказывать что 2+2=4 каждый раз заебывает
TK
Типичные zst инварианты в качестве пруфов
ΑZ
ну да, я и говорю что это в расте возможно. Это подмножество того что можно с пруфами завтиповыми но хоть что-то
TK
Главное, чтобы синглтонами оставались, а то можно случайно unsound
AN
так в итоге. главный вопрос так и осталься открыт. что есть завтипы.
ΑZ
завтипы это зависимые типы)))
B
это контракты
AN
ааа... хорош)))
TK
Типы, которые зав(исят от проверок на их собственных значениях)
TK
(простите за кривое определение)