| Require Import String. | |
| Inductive Term : nat -> Type := | |
| | App : forall {n m : nat}, Term (S n) -> Term m -> Term (n + m) | |
| | Fun : forall {n : nat}, Term 0 -> Term n -> Term (S n) | |
| | Var : string -> Term 0. |
A cartesian type is a generalized type product where one inhabitant, called origin is common to all the types involved (called axes). A cocartesian type is a generalized type sum with a common origin to all axes.
That is, A * ... * Z is a cartesian type if there exists one inhabitant i common to every axis — i_A = i_B = ... = i_Z.
# x is introduced to the environment
{ ..?e } → { x := 3 ; ..?e }
# y too ; ?e is not the same row variable as the one above
{ ..?e } → { y := 5 ; ..?e }
# matching the current context on one that contains an x and a y
# which allows us to add them to introduce y
{ x ; y ; ..?e } → { z := x + y ; ..?e }
| let ( or ) option default = Option.value option ~default | |
| module Int = struct | |
| include Int | |
| let compare i1 i2 = | |
| let as_int = compare i1 i2 in | |
| if as_int > 0 then `Greater else if as_int < 0 then `Less else `Equal | |
| ;; |
| type inhabited = Inhabited | |
| module Hole = struct | |
| (* Discriminator for Done *) | |
| type 'ty value = Value of 'ty | |
| (* Discriminator for Falling *) | |
| type nonterm = Nonterm | |
| type 'value t = |
| #!/usr/bin/env -S neige run | |
| extend Nat with module | |
| # This version does not care about a leading zero | |
| let parse_decimal_digits : String -> List Nat = | |
| let tailrec string acc = | |
| match string with | |
| | "" -> acc | |
| | ('0' .. '9' as first) :: rest -> | |
| let digit = Char.code_point_of first - Char.digit_offset in |
| # ruff: noqa: S101, PLR6301, RUF002 | |
| """ | |
| Cursed implementation of `is_odd`. | |
| It relies on two interesting properties. Firstly, the set formed | |
| by the difference of consecutive squares is the odd members of | |
| ℕ - let's call this set ℕ_odd. | |
| Secondly, the negative integers are symmetric to their positive | |
| counterparts with respect to oddness. Differently put, negating | |
| a number preserves the fact that it is odd. |
| (* we start by setting up a global scope. | |
| `setup` is a special function that handles all we need behind | |
| the scenes. `$global` is a macro that gets substituted with | |
| the scope ID from the meta-environment mapping (ID -> scope) *) | |
| $global -> setup () | |
| (* `let` is an applicative statement that handles intro and | |
| substitution in the specified scope *) | |
| let($global) n := 3 |
| public Nat -> type | |
| | O : Nat | |
| | S : Nat -> Nat | |
| public successor -> fun (n : Nat) : Nat => S n | |
| public predecessor -> fun (S n : Nat) : Nat => n | |
| public n + m -> | |
| split n, m into | |
| | _, O -> n |
| {-# LANGUAGE MonoLocalBinds #-} | |
| module Main where | |
| class Relation r a b | |
| class Relation r a a => Reflexivity r a where | |
| reflexivity :: r a a | |
| class Relation r a b => Symmetry r a b where |