MevenBertrand

From Equations Require Import Equations.
From Coq Require Import Utf8 Program.Equality.

Unset Equations With Funext.


(* Partial function class *)
Class PFun {A} (f : A) := {
  psrc : Type ;
  ptgt : psrc → Type ;

MevenBertrand

Inductive expr : Set :=
  | var : nat -> expr
  | constr : expr -> expr -> expr
  | bad : expr.

Inductive wf_expr : expr -> Type :=
  | wf1_var n : wf_expr (var n)
  | wf1_constr e e' : wf_expr e -> wf_expr e' -> wf_expr (constr e e').

Class Wf := wf : expr -> Set.

MevenBertrand

Require Import Bool.

(* The base type is largely irrelevant, so I'll use bool instead of a custom type of terms *)
(* Also, I am defining just one kind of relation in each "family" (rel1/rel2/rel),
  but in reality each family would have ~10 different, mutually defined predicates/relations *)

Inductive rel1 : bool -> bool -> Set :=
  | crel1_true : rel1 true false
  | crel1_neg b b' : rel1 (negb b) (negb b') -> rel1 b b'.