inductive
definition
RoboticSubsystem
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Physics.RoboticsFromRS on GitHub at line 21.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
18
19namespace IndisputableMonolith.Physics.RoboticsFromRS
20
21inductive RoboticSubsystem where
22 | sensing | actuation | computation | communication | power
23 deriving DecidableEq, Repr, BEq, Fintype
24
25theorem roboticSubsystemCount : Fintype.card RoboticSubsystem = 5 := by decide
26
27/-- 6-DOF = cube faces = 6. -/
28def sixDOF : ℕ := 6
29theorem sixDOF_eq_cubefaces : sixDOF = 6 := rfl
30
31structure RoboticsCert where
32 five_subsystems : Fintype.card RoboticSubsystem = 5
33 six_dof : sixDOF = 6
34
35def roboticsCert : RoboticsCert where
36 five_subsystems := roboticSubsystemCount
37 six_dof := sixDOF_eq_cubefaces
38
39end IndisputableMonolith.Physics.RoboticsFromRS