File: bi_ascii_parsing.v

package info (click to toggle)
coq-iris 4.3.0-1
  • links: PTS, VCS
  • area: main
  • in suites: forky, sid, trixie
  • size: 4,116 kB
  • sloc: python: 130; makefile: 61; sh: 28; sed: 2
file content (39 lines) | stat: -rw-r--r-- 720 bytes parent folder | download | duplicates (2)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
Require Import Coq.Strings.String.
Require Import iris.bi.bi.
Require Import iris.bi.ascii.

Local Open Scope string_scope.

(* this file demonstrates that the [|-] notation does not
   conflict with the ltac notation.
 *)
Section with_bi.
  Context {PROP : bi}.
  Variables P Q R : PROP.

  Local Open Scope stdpp_scope.

  Ltac pg :=
    match goal with
    | |- ?X => idtac X
    end.

  Ltac foo g :=
    lazymatch g with
    | |- ?T => idtac T
    | ?U |- ?T => idtac U T
    end.

  Ltac bar :=
    match goal with
    | |- ?G => foo G
    end.

  Check "test1".
  Lemma test1 : |-@{PROP} True.
  Proof. bar. pg. Abort.

  Check "test2".
  Lemma test2 : False |-@{PROP} True.
  Proof. bar. pg. Abort.
End with_bi.