Documentation

Fp.Tactics

Imports

Init
Lean
Fp.Tactics.Attributes
Fp.Tactics.Simps

Imported by

Lean.ParserDescr

Equations

bvFloat = Lean.ParserDescr.node `bvFloat 1024 (Lean.ParserDescr.nonReservedSymbol "bv_float_normalize" false)

Instances For