-
Notifications
You must be signed in to change notification settings - Fork 0
Expand file tree
/
Copy pathLibString.v
More file actions
22 lines (17 loc) · 808 Bytes
/
LibString.v
File metadata and controls
22 lines (17 loc) · 808 Bytes
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
(* This file is extracted from the TLC library.
http://github.com/charguer/tlc
DO NOT EDIT. *)
(**************************************************************************
* TLC: A library for Rocq *
* Strings *
**************************************************************************)
Set Implicit Arguments.
From SLF Require Import LibTactics LibReflect.
Require Export Coq.Strings.String.
(* ********************************************************************** *)
(* ################################################################# *)
(** * Inhabited *)
#[global]
Instance Inhab_string : Inhab string.
Proof using. apply (Inhab_of_val EmptyString). Qed.
(* 2026-01-07 13:36 *)