damhiya

From Coq Require Import String.
From stdpp Require Import base strings.

Section AUX.

  #[global] Instance option_eq_dec_normalizable A `{dec : EqDecision A} : EqDecision (option A).
  Proof.
    intros x y. destruct x as [x|], y as [y|].
    - destruct (decide (x = y)).
      + left. congruence.

KiJeong-Lim

#include <cstdint>
#include "scratch.hpp"

struct MotorInput {
    float p;
    float v;
    float kp;
    float kd;
    float t_ff;
};