qexat

import enum
import typing

class Nat(enum.Enum):
    O = enum.auto()
    S = enum.auto()

type nat = typing.Literal[Nat.O] | tuple[typing.Literal[Nat.S], nat]

O = Nat.O

qexat

module Util = struct
  let ( let*? ) = Option.bind
  let ( let*! ) = Result.bind
  let ( let@ ) = ( @@ )
  let ( *> ) f g x = g (f x)
  let curry = ( @@ )
  let curry2 f a b = f (a, b)
  let curry3 f a b c = f (a, b, c)
  let ( let|> ) a k = a (curry k)
  let ( let||> ) a k = a (curry2 k)

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.