@[reducible, inline]

abbrev Physics.dim : ℕ

Equations

• Physics.dim = 2

@[reducible, inline]

abbrev Physics.Vec : Type

Equations

• Physics.Vec = (Fin Physics.dim → ℝ)

structure Physics.ParticleId : Type

• id : ℕ

def Physics.instDecidableEqParticleId.decEq (x✝ x✝¹ : ParticleId) : Decidable (x✝ = x✝¹)

Equations

• Physics.instDecidableEqParticleId.decEq { id := a } { id := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Physics.instDecidableEqParticleId : DecidableEq ParticleId

Equations

• Physics.instDecidableEqParticleId = Physics.instDecidableEqParticleId.decEq

@[instance_reducible]

instance Physics.instHashableParticleId : Hashable ParticleId

Equations

• Physics.instHashableParticleId = { hash := Physics.instHashableParticleId.hash }

def Physics.instHashableParticleId.hash : ParticleId → UInt64

Equations

• Physics.instHashableParticleId.hash { id := a } = mixHash 0 (hash a)

@[instance_reducible]

instance Physics.instInhabitedParticleId : Inhabited ParticleId

Equations

• Physics.instInhabitedParticleId = { default := { id := default } }

structure Physics.Particle : Type

• id : ParticleId
• radius : ℝ
• mass : ℝ
• position : Vec
• velocity : Vec
• cVelocity : Option Vec
• resting : Bool
• restRef : Set' ParticleId
• restRefC : Set' ParticleId

class Physics.Particle.WF (p : Particle) : Prop

• radius_pos : 0 < p.radius
• mass_pos : 0 < p.mass

@[instance_reducible]

instance Physics.instInhabitedParticle : Inhabited Particle

Equations

• Physics.instInhabitedParticle = { default := { id := { id := 0 }, radius := 1, mass := 1, position := 0, velocity := 0, cVelocity := none, resting := false, restRef := ∅, restRefC := ∅ } }

instance Physics.instWFDefaultParticle : default.WF

def Physics.Particle.overlaps (p₁ p₂ : Particle) : Prop

Equations

• p₁.overlaps p₂ = (‖p₁.position - p₂.position‖ = 0)

structure Physics.Simulator : Type

• particles : Map ParticleId Particle

class Physics.Simulator.WF (sim : Simulator) : Prop

• particle_id_eq {i : ParticleId} {p : Particle} : Map.get? i sim.particles = some p → p.id = i

@[instance_reducible]

instance Physics.instInhabitedSimulator : Inhabited Simulator

Equations

• Physics.instInhabitedSimulator = { default := { particles := ∅ } }

instance Physics.instWFDefaultSimulator : default.WF