FiniteStateMachines

Difficulty: easy — 2 definitions, 0 abbreviations, 0 lemmas, 0 theorems, 0 examples.

definition
legend
sequential-circuits
FiniteStateMachine (State Input Output : Type) [Fintype State] [Fintype Input] [Fintype Output]
  [Nonempty State] [Nonempty Input] [Nonempty Output] : Type
Show details 
| FiniteStateMachine.mk : {State Input Output : Type} →
  [inst : Fintype State] →
    [inst_1 : Fintype Input] →
      [inst_2 : Fintype Output] →
        [inst_3 : Nonempty State] →
          [inst_4 : Nonempty Input] →
            [inst_5 : Nonempty Output] →
              (State → Input → State × Output) → FiniteStateMachine State Input Output

Outer dependencies: (none)

Mathlib dependencies: Fintype

Lean core dependencies: Eq, HEq, Nat, Nonempty, Prod, SizeOf, eq_of_heq

Used by: FiniteStateMachine.Reversible

FiniteStateMachine.Reversible {State Input Output : Type} [Fintype State] [Fintype Input]
  [Fintype Output] [Nonempty State] [Nonempty Input] [Nonempty Output]
  (fsm : FiniteStateMachine State Input Output) : Prop
Show details 
fun {State Input Output} [Fintype State] [Fintype Input] [Fintype Output] [Nonempty State]
    [Nonempty Input] [Nonempty Output] fsm =>
  Function.Injective fun p => fsm.step p.1 p.2

Complexity: 107 (size of the value term)

Outer dependencies: FiniteStateMachine

Mathlib dependencies: Fintype

Lean core dependencies: Function.Injective, Nonempty, Prod

Used by: (none)

Dependency diagram

Drag to pan, Ctrl+scroll (or Cmd+scroll, or pinch on a touch screen) to zoom, click a node to jump to it.

definitiondeclared elsewheredependencyproof dependency
legend