Sign in
◑
Theme
fuchsia
/
third_party
/
github.com
/
leanprover
/
lean4
/
refs/heads/upstream/expose-array-back
/
.
/
tests
/
elab
/
unusedWarningAtStructUpdate.lean
blob: e75f7e85a6f1f287923e8539bab156c24e19605d [
file
] [
edit
]
set_option linter
.
unusedVariables
true
structure
Ctx
where
s
:
String
def
f
(
s
:
String
)
:
ReaderT
Ctx
Id
Unit
:=
withReader
(
fun ctx
=>
{
ctx
with
s
:=
s
})
(
pure
())