qexat

type left = private Left_tag
type right = private Right_tag

type ('ctr, 'left, 'right) t =
  | Left : 'a 'b. 'a -> (left, 'a, 'b) t
  | Right : 'a 'b. 'b -> (right, 'a, 'b) t

let introduction_left : type a b. a -> (left, a, b) t =
  fun a -> Left a

qexat

e ::= x
    | '(' e ')'
    | e e
    | 'λ' x '.' e
---------------------------------------------------------------
_&>_ a b = a ∧ (a → b)

or_elim = (a → c) → (b → c) → a ∨ b → c
or_elim f _ (Left a) = f a
or_elim _ g (Right b) = g b

qexat

use it in pyright: playground link

qexat

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE UndecidableSuperClasses #-}

import Data.Kind

class (c a, c b) => SafeCoercible (c :: Type -> Constraint) a b | c a -> b where
  safeCoerce :: a -> b

instance SafeCoercible Num Int Float where

qexat

%%%%%%%%%%%%%%%%%%%%%%%%
% the bug fix workflow %
%%%%%%%%%%%%%%%%%%%%%%%%

=========================
what does a bug fix have?
=========================

-> a name that can be referenced
-> a description to use in commit & release

qexat

module False = struct
  (** This empty type represents falsehood. No proof (term) of
      it exists. *)
  type t = |

  (** [ex_falso_quodlibet] states that if we have the proof of
      falsehood, then we can prove anything. *)
  let ex_falso_quodlibet : 'a. t -> 'a = function
    | _ -> .
end

qexat

induct _=_ {T} _ _ ≔
  rule reflexivity x. (x : T) -> (Refl x : x = x)
with module
  rule symmetry x y. x = y -> y = x ≔ λ (Refl x) → Refl x
  rule transitivity x y z. x = y -> y = z -> x = z ≔
    fun x-=-y y-=-z → (x-=-y)[ϕ y-=-z]
end

induct _×_ A B ≔
  rule pair x y. (x : A) -> (y : B) -> ('(x, y') : A × B) 

qexat

Require Import Arith.

Lemma max_override_right : forall (n m p : nat), (n >= m) -> max n (max m p) = max n p.
Proof.
  intros n m p ge_n_m.

  inversion ge_n_m ; rewrite Nat.max_assoc.
  - rewrite Nat.max_id.
    reflexivity.
  - rewrite H0.

qexat

data Nat where
  O :: Nat
  S :: Nat -> Nat

instance Eq Nat where
  (==) O O = True
  (==) O (S _) = False
  (==) (S _) O = False
  (==) (S n) (S m) = n == m

qexat

let ( let+ ) = Option.bind

module Expr = struct
  type app = A
  type fun' = F
  type name = N
  type 'variant reducible = A : app reducible

  type 'variant irreducible =
    | F : fun' irreducible