amarmaduke

module example1.

import stdlib.

compose : ∀ A:★. ∀ B:★. ∀ C:★. (B ➔ C) ➔ (A ➔ B) ➔ A ➔ C
= Λ A. Λ B. Λ C. λ g. λ f. λ x. g (f x).

data Tree : ★ =
| leaf : Nat ➔ Tree
| node : Tree ➔ Nat ➔ Tree ➔ Tree

amarmaduke

use std::hash;
use std::ops::Deref;
use std::ptr;
use std::rc::{Rc, Weak};

use hashbrown::HashMap;

#[derive(Debug, Clone)]
pub struct Hc<T>(Rc<T>);

amarmaduke

Require Import List.
Require Import Nat.
Require Import Bool.
Import ListNotations.

Inductive subseq : list nat -> list nat -> Prop :=
  | hl1 : subseq [] []
  | hl2 lst1 lst2 (H: subseq lst1 lst2) : forall (x : nat),
      subseq lst1 (x :: lst2)
  | hl3 lst1 lst2 (H: subseq lst1 lst2) : forall (x : nat),

amarmaduke

[package]
name = "scratch"
version = "0.1.0"
edition = "2021"

# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html

[dependencies]
bumpalo = "3.9.1"
threadstack = "0.4.1"

amarmaduke

use std::time;

use tailcall::tailcall;

enum Nat {
    Zero,
    Succ(Box<Nat>)
}

amarmaduke

import stdlib.

module ords (U:Nat ➔ ★).

opaque U_zero_is_unit : TpEq·(U zero)·Unit = ●.

data Ord : ★ =
| base : Ord
| next : Π n:Nat. U n ➔ Ord.

amarmaduke

import stdlib.
module test.

SFalse : ★ ➔ ★ = λ A:★. Cast·A·Unit.

good : ∀ A:★. SFalse·A ➾ SFalse·A
= Λ A. Λ f. intrCast -(cast -f) -(λ _. β).

bad : ∀ A:★. SFalse·A ➾ SFalse·A
= Λ A. Λ f. irrelCast·A·Unit -f. 

amarmaduke

module Test

open FStar.Mul

type nat = x:int{x >= 0}

let double (x:int) = x + x

val factorial : nat -> Tot nat

amarmaduke

module test where

data Id {A : Set} (x : A) : A → Set where
  refl : Id x x 

data ExtId : (A : Set) → A → A → Set1 where
  def : (A : Set) → (x : A) → (y : A) → Id x y → ExtId A x y
  fun : (A : Set) → (B : Set) → (x : A → B) → (y : A → B) → (ext : (z : A) → ExtId B (x z) (y z)) → ExtId (A → B) x y

amarmaduke

with import <nixpkgs> {}; {
   odinEnv = stdenv.mkDerivation {
      name = "odin";
      buildInputs = [stdenv xorg.libX11 xorg.libXcursor xorg.libXxf86vm xorg.libXi xlibsWrapper rustc cargo];
   };
}