This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
(* | |
* Copyright (C) BedRock Systems Inc. 2020-22 | |
* | |
* This software is distributed under the terms of the BedRock Open-Source License. | |
* See the LICENSE-BedRock file in the repository root for details. | |
*) | |
Require Export stdpp.fin_sets. | |
Require Export iris.prelude.prelude. | |
(** * Small extensions to [stdpp.fin_sets]. *) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Require Import List. | |
Import ListNotations. | |
Lemma test1 : | |
length ([1] ++ [2]) = 2 -> | |
2 = 4. | |
Proof. | |
intros HA. | |
evar (N : nat). |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
``` | |
$ git rev-parse HEAD | |
e31304d4d76d616130bc635457f12d5a6878b3d8 | |
$ dune test --display verbose test/blackbox-tests/test-cases/promote/ | |
Shared cache: enabled | |
Workspace root: /Users/pgiarrusso1/git-bedrock/dune | |
Running[0]: /Users/pgiarrusso1/git-bedrock/dune/_opam/bin/ocamlc.opt -config > /var/folders/6q/2ycxnczj1qsgwsk7lg3yd4bh0000gn/T/dune_f0778e_output | |
Dune context: | |
{ name = "default" | |
; kind = "default" |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Require Import iris.proofmode.proofmode. | |
Lemma string_fun (PROP : bi) (X : PROP) : X ⊢ X. | |
Proof. | |
iIntros "X". | |
generalize true; intros. | |
Show. | |
(* | |
1 goal |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
(* | |
* Copyright (c) 2021 BedRock Systems, Inc. | |
* | |
* This software is distributed under the terms of the BedRock Open-Source License. | |
* See the LICENSE-BedRock file in the repository root for details. | |
*) | |
From stdpp Require Export finite. | |
From bedrock.prelude Require Import base bool numbers list_numbers gmap list fin_sets. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
dune build -p elpi -j 11 @all | |
(cd _build/default && /Users/pgiarrusso1/.opam/4.14.0+trunk/bin/ocamlc.opt -linkall -g -bin-annot -I src/.elpi.objs/byte -I src/.elpi.objs/public_cmi -I /Users/pgiarrusso1/.opam/4.14.0+trunk/lib/camlp5 -I /Users/pgiarrusso1/.opam/4.14.0+trunk/lib/ppx_deriving/runtime -I /Users/pgiarrusso1/.opam/4.14.0+trunk/lib/re -I /Users/pgiarrusso1/.opam/4.14.0+trunk/lib/re/str -I /Users/pgiarrusso1/.opam/4.14.0+trunk/lib/result -I /Users/pgiarrusso1/.opam/4.14.0+trunk/lib/seq -I /Users/pgiarrusso1/.opam/4.14.0+trunk/lib/stdlib-shims -I trace/runtime/.trace_ppx_runtime.objs/byte -no-alias-deps -open Elpi__ -o src/.elpi.objs/byte/elpi__Parser.cmi -c -intf src/parser.pp.mli) | |
File "src/parser.mli", line 34, characters 89-102: | |
34 | val parse_program_from_stream : parser_state -> print_accumulated_files:bool -> Loc.t -> char Stream.t -> Program.t | |
^^^^^^^^^^^^^ | |
Alert deprecated: module Stdlib.Stream | |
Use th |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
(* | |
Tested with: | |
Coq 8.15.0, Iris dev.2022-01-24.0.72a4bd62. | |
Coq 8.16.0, Iris 4.0.0 | |
*) | |
From iris.prelude Require Import prelude. | |
Lemma bar : (if decide (0 = 0) then 0 else 0) = 0. | |
Proof. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Require Import stdpp.base. | |
Module Type FOO. | |
Definition number : Set := nat. | |
End FOO. | |
Module Import foo : FOO. | |
Definition number : Set := nat. | |
Fail #[global] Instance number_inh : Inhabited number := _. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Require Import stdpp.base. | |
Require Import NArith. | |
(* We omit [Require Import stdpp.numbers.], which already has the [Inhabited] | |
instances we test here. *) | |
Module Type X. | |
#[global] Instance a : Inhabited nat. | |
Proof. | |
Fail apply _. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
(* Distributed under the terms of the MIT license. *) | |
From Coq Require Import CMorphisms. | |
From MetaCoq.Template Require Import config utils Reflect Ast AstUtils Induction LiftSubst Reflect. | |
Require Import ssreflect. | |
From Equations.Prop Require Import DepElim. | |
Set Equations With UIP. | |
Definition R_universe_instance R := | |
fun u u' => Forall2 R (List.map Universe.make u) (List.map Universe.make u'). |