Commit 224229c4 authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

PVS driver: some explanation regarding 'const'

parent 7e3e563b
......@@ -38,8 +38,11 @@ theory map.Map
remove prop Select_eq
remove prop Select_neq
syntax function const "(LAMBDA (x:%t0): %1)"
(* %t0 is "map a b"
%t1 is the type of const's argument, that is "b"
but we need type "a" instead, i.e. the first type argument
syntax function const "(LAMBDA (x:%t1): %1)"
remove prop Const
......@@ -12,11 +12,6 @@ theory TestPVS
goal G: get (const False) 42 = False
use import real.Real
use import real.Power
goal G1: pow 2. 4. = 16.
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment