Library Malfunction.Examples.simple.test_plugin

From Malfunction Require Import FFI.
From VerifiedExtraction Require Import Extraction.
From MetaRocq.Utils Require Import bytestring MRString.
Local Open Scope bs.
Definition test (x : unit) := coq_msg_info "Hello world!".

Set Warnings "-primitive-turned-into-axiom".

From Stdlib Require Import PrimFloat.
Definition test_float : float := abs (1000%float).
Verified Extraction -typed -unsafe -time -fmt -compile-plugin -load test_float.

Verified Extraction -typed -unsafe -time -fmt -compile-plugin -run (abs 1.5%float).