Skip to content

Commit f52cc70

Browse files
committed
Add support for sqrt, log and expr
1 parent f66de1d commit f52cc70

1 file changed

Lines changed: 6 additions & 2 deletions

File tree

‎RandomDo/Tactic/Computable/Counterparts.lean‎

Lines changed: 6 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -27,8 +27,12 @@ attribute [computable_as Float] NNReal
2727

2828
/-! ## Distributions -/
2929

30-
/- `gaussianReal` reads its second argument as a variance and `normal` reads it as a standard
31-
deviation: the two agree on the `1` the example draws with, not in general. -/
3230
attribute [computable_as NumLean.normal'] ProbabilityTheory.gaussianReal
3331

32+
attribute [computable_as Float.sqrt] Real.sqrt
33+
34+
attribute [computable_as Float.log] Real.log
35+
36+
attribute [computable_as Float.exp] Real.exp
37+
3438
end

0 commit comments

Comments
 (0)