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

State before:
R : Type
inst✝⁵ : RealScalar R
W : Type ?u.33122
inst✝⁴ : SemiHilbert R W
X : Type ?u.33152
inst✝³ : SemiHilbert R X
Y : Type ?u.33176
inst✝² : SemiHilbert R Y
Z : Type ?u.33200
inst✝¹ : SemiHilbert R Z
inst✝ : MeasureSpace R
t : R
⊢ foo2 t = if 0 < t ∧ t < 1 then 1 else 0
Tactic:
rfl
State after:
no goals