source: src/utilities/hide.ma @ 2896

Last change on this file since 2896 was 2200, checked in by tranquil, 7 years ago
  • updated joint semantics: generation of linear and graph semantics
  • opened two axioms in BitVectorZ
File size: 1.2 KB
Line 
1(**************************************************************************)
2(*       ___                                                              *)
3(*      ||M||                                                             *)
4(*      ||A||       A project by Andrea Asperti                           *)
5(*      ||T||                                                             *)
6(*      ||I||       Developers:                                           *)
7(*      ||T||         The HELM team.                                      *)
8(*      ||A||         http://helm.cs.unibo.it                             *)
9(*      \   /                                                             *)
10(*       \ /        This file is distributed under the terms of the       *)
11(*        v         GNU General Public License Version 2                  *)
12(*                                                                        *)
13(**************************************************************************)
14
15include "basics/logic.ma".
16
17definition hide_prf : ∀P : Prop.P → P ≝ λP,prf.prf.
18definition hide_Prop : Prop → Prop ≝ λP.P.
19
20interpretation "hide proof" 'hide p = (hide_prf ? p).
21interpretation "hide Prop" 'hide p = (hide_Prop p).
Note: See TracBrowser for help on using the repository browser.