|
Require Import Coq.ZArith.ZArith.
Require Import Coq.micromega.Lia.
Local Open Scope Z_scope.
Definition Register := Z%type.
Definition Opcode := Z%type.
Inductive InstructionI : Type
:= Lb : Register -> Register -> Z -> InstructionI
| InvalidI : InstructionI.
Inductive Instruction : Type
:= IInstruction : InstructionI -> Instruction.
Definition funct3_LB : Z := 0.
Definition opcode_LOAD : Opcode := 3.
Set Universe Polymorphism.
Definition MachineInt := Z.
Definition funct3_JALR := 0.
Axiom InstructionMapper: Type -> Type.
Definition apply_InstructionMapper(mapper: InstructionMapper Z)(inst: Instruction): Z :=
match inst with
| IInstruction InvalidI => 2
| IInstruction (Lb rd rs1 oimm12) => 3
end.
Axiom Encoder: InstructionMapper MachineInt.
Definition encode: Instruction -> MachineInt := apply_InstructionMapper Encoder.
Lemma foo: forall (ins: InstructionI),
0 <= encode (IInstruction ins) ->
0 <= encode (IInstruction ins) .
Proof.
Set Printing Universes.
intros.
lia.
Qed.
¤ Dauer der Verarbeitung: 0.20 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
