mukeshtiwari

(**
Skip to [Definition decode_aux] to see the main definition.
*)

Require Import Coq.Lists.List.
Require Import Coq.Relations.Relation_Operators.
Require Import Coq.Wellfounded.Lexicographic_Product.
Require Import Coq.Arith.Wf_nat.
Import ListNotations.
Require Import Coq.Init.Nat.

mukeshtiwari

mukeshtiwari@Mukeshs-MacBook-Pro exercises % make
coq_makefile -f _CoqProject -o Makefile.coq
/Library/Developer/CommandLineTools/usr/bin/make -f Makefile.coq
COQDEP VFILES
*** Warning: in file MetaCoqPrelude.v, library All is required from root MetaCoq.Template and has not been found in the loadpath!
*** Warning: in file MetaCoqPrelude.v, library Checker is required from root MetaCoq.Template and has not been found in the loadpath!
*** Warning: in file MetaCoqPrelude.v, library Reduction is required from root MetaCoq.Template and has not been found in the loadpath!
*** Warning: in file ./MetaCoqPrelude.v, library All is required from root MetaCoq.Template and has not been found in the loadpath!
*** Warning: in file ./MetaCoqPrelude.v, library Checker is required from root MetaCoq.Template and has not been found in the loadpath!
*** Warning: in file ./MetaCoqPrelude.v, library Reduction is required from root MetaCoq.Template and has not been found in the loadpath!

mukeshtiwari

Require Import Coq.Lists.List.
Require Import Coq.Relations.Relation_Operators.
Require Import Coq.Wellfounded.Lexicographic_Product.
Require Import Coq.Arith.Wf_nat.
Import ListNotations.
Require Import Coq.Init.Nat.

Require Import Lia.
Require Import Relation_Definitions.

mukeshtiwari

Require Import Coq.Lists.List.
Require Import Coq.Relations.Relation_Operators.
Require Import Coq.Wellfounded.Lexicographic_Product.
Require Import Coq.Arith.Wf_nat.
Import ListNotations.
Require Import Coq.Init.Nat.

Require Import Lia.
Require Import Relation_Definitions.

mukeshtiwari

Require Import Coq.Lists.List.
Require Import Coq.Relations.Relation_Operators.
Require Import Coq.Wellfounded.Lexicographic_Product.
Require Import Coq.Arith.Wf_nat.
Import ListNotations.
Require Import Coq.Init.Nat.

Require Import Lia.
Require Import Relation_Definitions.

mukeshtiwari

Project C is big (4th year project, 3 months full time) and Project B is small (3rd year student, 1 month full time). 

mukeshtiwari

#!/bin/bash
# Sometimes you need to move your existing git repository
# to a new remote repository (/new remote origin).
# Here are a simple and quick steps that does exactly this.
#
# Let's assume we call "old repo" the repository you wish
# to move, and "new repo" the one you wish to move to.
#
### Step 1. Make sure you have a local copy of all "old repo"
### branches and tags.

mukeshtiwari

Require Import Field_theory 
  Ring_theory List NArith 
  Ring Field Utf8 Lia Coq.Arith.PeanoNat. 
Import ListNotations.

Section Computation.

  

mukeshtiwari

Require Import List Utf8 Vector Fin Psatz.
Import Notations ListNotations.

Require Import Lia
  Coq.Unicode.Utf8
  Coq.Bool.Bool
  Coq.Init.Byte
  Coq.NArith.NArith
  Coq.Strings.Byte
  Coq.ZArith.ZArith

mukeshtiwari

(* This is with Set Printing All *)

Error: Abstracting over the term "np <? 256" leads to a term
λ b : bool,
  ∀ f : ∀ mp : N, np = mp → (mp <? 256) = false → byte,
    (if b as b0 return (∀ mp : N, np = mp → (mp <? 256) = b0 → byte)
     then
      λ (mp : N) (Hmp : np = mp) (Hmpt : (mp <? 256) = true),
        match of_N mp as npt return (of_N mp = npt → byte) with
        | Some x0 => λ _ : of_N mp = Some x0, x0