Minuska.builtin.bool_signature

From Minuska Require Import
    prelude
    spec
.

Variant BoolFunSymbol :=
| bool_fun_true
| bool_fun_false
| bool_fun_neg
| bool_fun_and
| bool_fun_or
| bool_fun_iff
| bool_fun_xor
.

Variant BoolPredSymbol :=
| bool_pred_is
| bool_pred_is_false
| bool_pred_is_true
.

#[export]
Instance BoolFunSymbol_eqdec : EqDecision BoolFunSymbol.
Proof.
    ltac1:(solve_decision).
Defined.

#[export]
Instance BoolPredSymbol_eqdec : EqDecision BoolPredSymbol.
Proof.
    ltac1:(solve_decision).
Defined.

#[export]
Program Instance BoolFunSymbol_fin : Finite BoolFunSymbol := {|
    enum := [
        bool_fun_true;
        bool_fun_false;
        bool_fun_neg;
        bool_fun_and;
        bool_fun_or;
        bool_fun_iff;
        bool_fun_xor
    ]
|}.
Next Obligation.
    (repeat constructor); ltac1:(set_solver).
Qed.
Next Obligation.
    destruct x; ltac1:(set_solver).
Qed.
Fail Next Obligation.

#[export]
Program Instance BoolPredSymbol_fin : Finite BoolPredSymbol := {|
    enum := [
        bool_pred_is;
        bool_pred_is_false;
        bool_pred_is_true
    ]
|}.
Next Obligation.
    (repeat constructor); ltac1:(set_solver).
Qed.
Next Obligation.
    destruct x; ltac1:(set_solver).
Qed.
Fail Next Obligation.
(* 
Definition bool_signature : Signature := {|
    FunSymbol := BoolFunSymbol ;
    PredSymbol := BoolPredSymbol ;
|}. *)