Theorem: SciLean.foo1_spec (SciLean/Core/Distribution/SimpleExamples.lean)

State before:
R : Type
inst✝⁵ : RealScalar R
W : Type ?u.13209
inst✝⁴ : SemiHilbert R W
X : Type ?u.13239
inst✝³ : SemiHilbert R X
Y : Type ?u.13263
inst✝² : SemiHilbert R Y
Z : Type ?u.13287
inst✝¹ : SemiHilbert R Z
inst✝ : MeasureSpace R
t : R
⊢ foo1 t = if 0 < t ∧ t < 1 then 1 else 0
Tactic:
rfl
State after:
no goals