pedrotst

From Coq Require Lists.List.

Import Lists.List.ListNotations.
Require Import Arith.

Require Import Coq.Program.Wf.

Program Fixpoint nat_to_bin (n : nat) {measure n}: list nat :=
  match n with
  | 0 => [0]

pedrotst

(* Let's define an eqdec function to decide if two natural numbers are the
same *)
Fixpoint myeqdec_fun (n m : nat) : Prop :=
  match (n, m) with
  | (0, 0) => True
  | (S n, S m) => myeqdec_fun n m
  | _ => False
  end.

(* Notice that it is computable, meaning that we can run it: *)

pedrotst

✔️ File './Alpha_context.v' successfully generated
Fatal error: exception Invalid_argument("List.fold_left2")
Raised at file "stdlib.ml", line 30, characters 20-45
Called from file "src/type.ml", line 99, characters 18-211
Called from file "src/monadEval.ml", line 119, characters 13-24
Called from file "src/monadEval.ml", line 119, characters 8-32
Called from file "src/monadEval.ml", line 117, characters 8-22
Called from file "src/monadEval.ml", line 117, characters 8-22
Called from file "src/monadEval.ml", line 119, characters 8-32
Called from file "src/monadEval.ml", line 119, characters 8-32

pedrotst

module test.
data list (A : ★) : ★ =
  | nil : list
  | cons : A ➔ list ➔ list.

list_ind : ∀ A : ★ . ∀ P : Π l : list ·A . ★ . Π f : P (nil ·A) . Π f' : Π a : A . Π l : list ·A . P l ➔ P (cons ·A a l) . Π l : list ·A . P l = Λ A : ★ . Λ P : Π l : list ·A . ★ . λ f : P (nil ·A) . λ f' : Π a : A . Π l : list ·A . P l ➔ P (cons ·A a l) . λ l : list ·A . μ F. l @(λ l : list ·A . P l) {
  | nil ➔ f 
  | cons y l' ➔ f' y (to/list -isType/F l') (F l') 
 }.

pedrotst

  Inductive A : Type := foo_A : nat -> A.
  Inductive B : Type := foo_B : bool -> B.

  Fixpoint fa (a : A) {struct a} : nat := match a with | foo_A x => x end
  with fb (b: B) {struct b} : bool := match b with | foo_B b => b end
  with fab (ab : A + B) {struct ab} : nat + bool :=
  match ab with
  | inl a => inl (fa a)
  | inr b => inr (fb b)
end.

pedrotst

Require Import MetaCoq.Template.Loader.

Quote Recursively Definition list_syntax := 
ltac:(let t := eval compute in list in exact t).

Make Definition list_from_syntax :=
  ltac:(let t := eval cbv in list_syntax in exact t).

(*
Error:

pedrotst

(* Assume we want to do some sort of "qualified import" *)
(* According to this thread [https://coq-club.inria.narkive.com/Nr2nabab/qualified-imports] *)
(* we can do the following two ways: *)
Require List.
Require Vector.

(* This is the first way *)
Module L := Vector.

Print L

pedrotst

/Library/Developer/CommandLineTools/usr/bin/make -C template-coq
coq_makefile -f _CoqProject -o Makefile.coq
/Library/Developer/CommandLineTools/usr/bin/make -f Makefile.coq
COQDEP VFILES
COQC theories/utils.v
COQC theories/config.v
COQC theories/BasicAst.v
COQC theories/Universes.v
COQC theories/Ast.v
COQC theories/AstUtils.v

pedrotst

#include <stdint.h>

uint32_t ffs_ref(uint32_t word) {
  if(!word) return 0;
  for(int c = 0, i = 0; c < 32; c++)
    if(((1 << i++) & word) != 0)
      return i;
  return 0;
}

pedrotst

Require Import List Arith.
Import ListNotations.

Class Referable (A: Set) :={
ref : A -> nat;
find: nat -> list A -> option A := 
  let fix f (key: nat) (l: list A) :=
  match l with
    | nil => None
    | (x :: xs) => if beq_nat key (ref x)