cppio

macro_rules! for_ {
    ($dollar:tt $ident:ident:$spec:tt in [$($tt:tt),+ $(,)?] $($item:tt)*) => {
        macro_rules! __for_body {
            ($dollar($dollar $ident:$spec),+) => {
                $dollar($($item)*)*
            }
        }
        __for_body! { $($tt),+ }
    }
}

cppio

//type F = f32;
//type U = u32;
type F = f64;
type U = u64;

pub fn sample_a(i: U) -> F {
    let d = 2.0 / F::EPSILON;
    (i % d as U) as F / d
}

cppio

def beq_of_eq {α : Type u} [BEq α] [LawfulBEq α] {a b : α} : a = b → a == b := (· ▸ LawfulBEq.rfl)

instance [BEq α] [LawfulBEq α] : DecidableEq α
  | x, y => if h : x == y then isTrue (eq_of_beq h) else isFalse (h ∘ beq_of_eq)

cppio

variable {α : Sort u} {β : α → Sort v} (f g : (x : α) → β x)

def eqv := ∀ x, f x = g x

theorem eq_of_eqv (h : eqv f g) : f = g :=
  congrArg (λ x => ·.lift (· x) (λ _ _ => (· x))) (Quot.sound h)

cppio

inductive ℕ
  | z
  | s (n : ℕ)

theorem ℕ.s_inj : s n = s m → n = m :=
  Eq.rec (motive := λ m _ => rec False (λ m _ => n = m) m) rfl

theorem ℕ.s_ne_z : s n ≠ z :=
  Eq.rec (motive := λ m _ => rec False (λ _ _ => True) m) trivial

cppio

set_option inductive.autoPromoteIndices false

variable {α : Type}

inductive Eq₁ : (x y : α) → Type
  | refl : Eq₁ x x

inductive Eq₂ x : (y : α) → Type
  | refl : Eq₂ x x

cppio

#![feature(
    associated_const_equality,
    const_float_bits_conv,
    const_trait_impl,
    generic_const_exprs,
    trait_alias
)]
use core::{
    fmt::{self, Display},
    ops::{Add, Div, Mul, Sub},

cppio

use core::ops::{Add, Div, Mul, Rem, Sub};
use num::{traits::NumOps, One, Rational32};

#[derive(Clone, Copy)]
struct Dual<T> {
    x: T,
    d: T,
}

impl<T: One> Dual<T> {

cppio

import operator, math

class Vector:
    def __init__(self, *v):
        self.v = tuple(v)

    def __repr__(self):
        return f"Vector{self.v}"

    def _op(op):

cppio

bool oeq(float x, float y) { return x == y; }
bool ogt(float x, float y) { return x > y; }
bool oge(float x, float y) { return x >= y; }
bool olt(float x, float y) { return x < y; }
bool ole(float x, float y) { return x <= y; }
bool one(float x, float y) { return !__builtin_isnan(x) & !__builtin_isnan(y) & x != y; }
bool ord(float x, float y) { return !__builtin_isnan(x) & !__builtin_isnan(y); }
bool uno(float x, float y) { return __builtin_isnan(x) | __builtin_isnan(y); }
bool ueq(float x, float y) { return __builtin_isnan(x) | __builtin_isnan(y) | x == y; }
bool ugt(float x, float y) { return !(x <= y); }