damhiya

From Coq Require Import String.
From stdpp Require Import base strings.

Section AUX.

  #[global] Instance option_eq_dec_normalizable A `{dec : EqDecision A} : EqDecision (option A).
  Proof.
    intros x y. destruct x as [x|], y as [y|].
    - destruct (decide (x = y)).
      + left. congruence.

damhiya

{-# OPTIONS --safe #-}
module Cubical.HITs.CauchyReal.Base where

open import Cubical.Foundations.Prelude
open import Cubical.Data.Rationals.Base
open import Cubical.Data.Rationals.Order
open import Cubical.Data.Rationals.Properties
open import Cubical.Data.PositiveRational.Base

-- Higher inductive-inductive construction of Cauchy real, as in the HoTT book.

damhiya

From Coq Require Import Lia.

Section TERMINATION.

  Inductive terminate (P : nat -> Prop) : nat -> Prop :=
  | found : forall n, P n -> terminate P n
  | step : forall n, terminate P (S n) -> terminate P n
  .

  Fixpoint terminate_ind_dep

damhiya

Set Primitive Projections.

From Coq Require
  Program
  Logic.ProofIrrelevance
  Logic.PropExtensionality
  Logic.FunctionalExtensionality
  Logic.Epsilon
  Relations.Relation_Operators.

damhiya

From Coq Require Fin.

Definition ifun (X Y : nat -> Type) : Type := forall i, X i -> Y i.
Definition δ (X : nat -> Type) (n : nat) := X (S n).
Definition prod (X Y : nat -> Type) (n : nat) := (X n * Y n)%type.
Definition sum (X Y : nat -> Type) (n : nat) := (X n + Y n)%type.

Definition TermF' (X : nat -> Type) := sum (δ X) (prod X X).

Variant TermF (X : nat -> Type) : nat -> Type :=

damhiya

CoInductive bits : Set :=
| c0 : bits -> bits
| c1 : bits -> bits.

Lemma bits_eta : forall xs, match xs with
                     | c0 xs' => c0 xs'
                     | c1 xs' => c1 xs'
                     end = xs.
Proof.
  intro xs. destruct xs; reflexivity.

damhiya

data I = T | F
data TreeF :: (I -> Type) -> (I -> Type) where
  Tip    :: Int -> TreeF f T
  Forest :: f F -> TreeF f T
  Nil    :: TreeF f F
  Cons   :: f T -> f F -> TreeF f F

data Tree :: I -> Type where
  Fold :: TreeF Tree i -> Tree i

damhiya

let and = fn (b1 : bool) -> fn (b2 : bool) ->
            if b1 then b2 else false in
let or =  fn (b1 : bool) -> fn (b2 : bool) ->
            if b1 then true else b2 in
let map = fn (f : int * int * int -> int * int * int) ->
          fix (mapf : list (int * int * int) -> list (int * int * int)) xs ->
            case xs of
              { [] -> [] of (int * int * int)
              ; x :: xs -> f x :: mapf xs
              } in

damhiya

# Tetrahedron
# volume = 1/6
# area = (3 + sqrt 3)/2

tetrahedronMesh =
    let vmap = [ 0. 1. 0. 0.
               ; 0. 0. 1. 0.
               ; 0. 0. 0. 1.
               ]
        fmap = [ 0 0 0 1

damhiya

#!/usr/bin/env bash
PROFILE_PATH=/nix/var/nix/profiles

get_list() {
  find $PROFILE_PATH -type l \
  | awk "match(\$0, /^${PROFILE_PATH//\//\\\/}\/system-([0-9]*)-link\$/, res) { print res[1] }" \
  | sort
}

get_current() {