gdsfh

; create before first run:
(defun user-macro-file() "~/.emacs.d/custom-macros.el")

(load (user-macro-file))

(defun save-macro (name)                  
  "save a macro. Take a name as argument and save the last defined macro under this name at the end of your .emacs"
     (interactive "SName of the macro: ")  ; ask for the name of the macro    
     (kmacro-name-last-macro name)         ; use this name for the macro    
     (find-file (user-macro-file))         ; open ~/.emacs or other user init file 

gdsfh

Require Import String.
Definition named_goal (A : Type) (s : string) := A.
Notation _as s := (_ : named_goal _ s).


Tactic Notation "proving" "goal" constr(name) :=
  match goal with
  | |- named_goal _ name => unfold named_goal
  | _ => fail 1 "current goal is not '" name "'"
  end

gdsfh

Definition get_existent
  vt
  (k : kt)
 :
  forall (mr : list (kt * vt)) (H_in_mr : in_mr vt k mr), vt
.
refine
  ( (fix _self_ lst :=
       match lst as lst0 return in_mr vt k lst0 -> vt with
       | nil => fun Hin => (_as "nil")

gdsfh

Definition get_existent
  vt
  (k : kt)
  (mr : list (kt * vt))
  (H_in_mr : in_mr vt k mr)
 :
  vt
.
refine
  ( (fix _self_ lst (Hin : in_mr vt k lst) :=

gdsfh

Require Import String.
Definition named_goal (A : Type) (s : string) := A.
Notation _as s := (_ : named_goal _ s).

Tactic Notation "proving" "goal" constr(name) :=
  match goal with
  | |- named_goal _ name => unfold named_goal
  | _ => fail 1 "current goal is not '" name "'"
  end
.

gdsfh

Require Import List.

Inductive prop : list (bool * nat) -> Prop :=
| Case_cons : forall hb hn t, hb = true -> prop ((hb, hn) :: t)
| Case_nil : prop nil
.


Goal prop ((true, 0) :: nil).
apply Case_cons; reflexivity.

gdsfh

(*
Ltac users know that Ltac 'match' involves backtracking when one of match cases
has failed.  Sometimes it's undesirable, and Ltac code should fail without
checking other match branches.
Here is a dumb solution.
*)

Module Deep_fail.

Inductive deep_failure (A : Type) (s : A) : Type :=

gdsfh

Require Import List.

Section phoas.

Inductive type : Type :=
  | Tunit : type
  | Tint : option nat -> type
  | Tfunc : list type -> type -> type
.