max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

refactor: default ==> arbitrary

Browse source 
Make sure it is opaque, and avoid `irreducible`
This commit is contained in:
Leonardo de Moura 2019-11-05 14:42:42 -08:00
parent 06fe9d3afa
commit c3e9ac73e2
60 changed files with 184 additions and 187 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
library/Init/Control/EState.lean
View file

@ -36,7 +36,7 @@ namespace EStateM
variables {ε σ α β : Type u}
instance [Inhabited ε] : Inhabited (EStateM ε σ α) :=
⟨fun s => Result.error (default ε) s⟩
⟨fun s => Result.error (arbitrary ε) s⟩
@[inline] protected def pure (a : α) : EStateM ε σ α :=
fun s => Result.ok a s

2
library/Init/Control/Except.lean
View file

@ -19,7 +19,7 @@ inductive Except (ε : Type u) (α : Type v)
attribute [unbox] Except
instance {ε α : Type} [Inhabited ε] : Inhabited (Except ε α) :=
⟨Except.error (default ε)⟩
⟨Except.error (arbitrary ε)⟩
section
variables {ε : Type u} {α : Type v}

2
library/Init/Control/Monad.lean
View file

@ -31,7 +31,7 @@ instance monadInhabited' {α : Type u} {m : Type u → Type v} [Monad m] : Inhab
⟨pure⟩
instance monadInhabited {α : Type u} {m : Type u → Type v} [Monad m] [Inhabited α] : Inhabited (m α) :=
⟨pure $ default _⟩
⟨pure $ arbitrary _⟩
def joinM {m : Type u → Type u} [Monad m] {α : Type u} (a : m (m α)) : m α :=
bind a id

19
library/Init/Core.lean
View file

@ -1020,12 +1020,9 @@ structure PointedType :=
class Inhabited (α : Sort u) :=
(default : α)
constant default (α : Sort u) [Inhabited α] : α :=
constant arbitrary (α : Sort u) [Inhabited α] : α :=
Inhabited.default α
@[inline, irreducible] def arbitrary (α : Sort u) [Inhabited α] : α :=
default α
instance Prop.Inhabited : Inhabited Prop :=
⟨True⟩
@ -1033,7 +1030,7 @@ instance Fun.Inhabited (α : Sort u) {β : Sort v} [h : Inhabited β] : Inhabite
Inhabited.casesOn h (fun b => ⟨fun a => b⟩)
instance Forall.Inhabited (α : Sort u) {β : α → Sort v} [∀ x, Inhabited (β x)] : Inhabited (∀ x, β x) :=
⟨fun a => default (β a)⟩
⟨fun a => arbitrary (β a)⟩
instance : Inhabited Bool := ⟨false⟩
@ -1041,7 +1038,7 @@ instance : Inhabited True := ⟨trivial⟩
instance : Inhabited Nat := ⟨0⟩
instance : Inhabited NonScalar := ⟨⟨default _⟩⟩
instance : Inhabited NonScalar := ⟨⟨arbitrary _⟩⟩
instance : Inhabited PointedType := ⟨{type := PUnit, val := ⟨⟩}⟩
@ -1052,7 +1049,7 @@ protected def Nonempty.elim {α : Sort u} {p : Prop} (h₁ : Nonempty α) (h₂
Nonempty.rec h₂ h₁
instance nonemptyOfInhabited {α : Sort u} [Inhabited α] : Nonempty α :=
⟨default α⟩
⟨arbitrary α⟩
theorem nonemptyOfExists {α : Sort u} {p : α → Prop} : Exists (fun x => p x) → Nonempty α
| ⟨w, h⟩ => ⟨w⟩
@ -1195,10 +1192,10 @@ section
variables {α : Type u} {β : Type v}
instance Sum.inhabitedLeft [h : Inhabited α] : Inhabited (Sum α β) :=
⟨Sum.inl (default α)⟩
⟨Sum.inl (arbitrary α)⟩
instance Sum.inhabitedRight [h : Inhabited β] : Inhabited (Sum α β) :=
⟨Sum.inr (default β)⟩
⟨Sum.inr (arbitrary β)⟩
instance {α : Type u} {β : Type v} [DecidableEq α] [DecidableEq β] : DecidableEq (Sum α β) :=
{decEq := fun a b =>
@ -1219,7 +1216,7 @@ section
variables {α : Type u} {β : Type v}
instance [Inhabited α] [Inhabited β] : Inhabited (Prod α β) :=
⟨(default α, default β)⟩
⟨(arbitrary α, arbitrary β)⟩
instance [DecidableEq α] [DecidableEq β] : DecidableEq (α × β) :=
{decEq := fun ⟨a, b⟩ ⟨a', b'⟩ =>
@ -1710,7 +1707,7 @@ noncomputable def typeDecidableEq (α : Sort u) : DecidableEq α :=
noncomputable def typeDecidable (α : Sort u) : PSum α (α → False) :=
match (propDecidable (Nonempty α)) with
| (isTrue hp) => PSum.inl (@Inhabited.default _ (inhabitedOfNonempty hp))
| (isTrue hp) => PSum.inl (@arbitrary _ (inhabitedOfNonempty hp))
| (isFalse hn) => PSum.inr (fun a => absurd (Nonempty.intro a) hn)
noncomputable def strongIndefiniteDescription {α : Sort u} (p : α → Prop)

2
library/Init/Data/Array/Basic.lean
View file

@ -82,7 +82,7 @@ a.get ⟨i.toNat, h⟩
/- "Comfortable" version of `fget`. It performs a bound check at runtime. -/
@[extern "lean_array_get"]
def get! [Inhabited α] (a : @& Array α) (i : @& Nat) : α :=
if h : i < a.size then a.get ⟨i, h⟩ else default α
if h : i < a.size then a.get ⟨i, h⟩ else arbitrary α
def back [Inhabited α] (a : Array α) : α :=
a.get! (a.size - 1)

4
library/Init/Data/BinomialHeap/Basic.lean
View file

@ -68,8 +68,8 @@ else
/- O(log n) -/
@[specialize] def head [Inhabited α] (lt : α → α → Bool) : Heap α → α
| Heap.empty => default α
| Heap.heap [] => default α
| Heap.empty => arbitrary α
| Heap.heap [] => arbitrary α
| Heap.heap (h::hs) => hs.foldl (fun r n => if lt r n.val then r else n.val) h.val
@[specialize] def findMin (lt : α → α → Bool) : List (HeapNode α) → Nat → HeapNode α × Nat → HeapNode α × Nat

4
library/Init/Data/Hashable.lean
View file

@ -14,10 +14,10 @@ class Hashable (α : Type u) :=
export Hashable (hash)
@[extern "lean_usize_mix_hash"]
constant mixHash (u₁ u₂ : USize) : USize := default _
constant mixHash (u₁ u₂ : USize) : USize := arbitrary _
@[extern "lean_string_hash"]
protected constant String.hash (s : String) : USize := default _
protected constant String.hash (s : String) : USize := arbitrary _
instance : Hashable String := ⟨String.hash⟩
protected def Nat.hash (n : Nat) : USize :=

2
library/Init/Data/PersistentArray/Basic.lean
View file

@ -147,7 +147,7 @@ partial def popLeaf : PersistentArrayNode α → Option (Array α) × Array (Per
if h : cs.size ≠ 0 then
let idx : Fin cs.size := ⟨cs.size - 1, Nat.predLt h⟩;
let last := cs.get idx;
let cs := cs.set idx (default _);
let cs := cs.set idx (arbitrary _);
match popLeaf last with
| (none, _) => (none, emptyArray)
| (some l, newLast) =>

2
library/Init/Data/Random.lean
View file

@ -110,7 +110,7 @@ def IO.mkStdGenRef : IO (IO.Ref StdGen) :=
IO.mkRef mkStdGen
@[init IO.mkStdGenRef]
constant IO.stdGenRef : IO.Ref StdGen := default _
constant IO.stdGenRef : IO.Ref StdGen := arbitrary _
def IO.setRandSeed (n : Nat) : IO Unit :=
IO.stdGenRef.set (mkStdGen n)

2
library/Init/Data/String/Basic.lean
View file

@ -79,7 +79,7 @@ utf8ByteSize s
{str := s, startPos := 0, stopPos := s.bsize}
private def utf8GetAux : List Char → Pos → Pos → Char
| [], i, p => default Char
| [], i, p => arbitrary Char
| c::cs, i, p => if i = p then c else utf8GetAux cs (i + csize c) p
@[extern "lean_string_utf8_get"]

4
library/Init/Data/UInt.lean
View file

@ -274,9 +274,9 @@ def USize.ofUInt32 (a : UInt32) : USize := USize.ofNat (UInt32.toNat a)
def USize.ofUInt64 (a : UInt64) : USize := USize.ofNat (UInt64.toNat a)
-- TODO(Leo): give reference implementation for shift_left and shift_right, and define them for other UInt types
@[extern c inline "#1 << #2"]
constant USize.shift_left (a b : USize) : USize := USize.ofNat (default _)
constant USize.shift_left (a b : USize) : USize := USize.ofNat (arbitrary _)
@[extern c inline "#1 >> #2"]
constant USize.shift_right (a b : USize) : USize := USize.ofNat (default _)
constant USize.shift_right (a b : USize) : USize := USize.ofNat (arbitrary _)
def USize.lt (a b : USize) : Prop := a.val < b.val
def USize.le (a b : USize) : Prop := a.val ≤ b.val

14
library/Init/Fix.lean
View file

@ -19,10 +19,10 @@ bfix1 base rec usizeSz
fixCore1 base rec
@[inline] def fix1 {α β : Type u} [Inhabited β] (rec : (α → β) → α → β) : α → β :=
fixCore1 (fun _ => default β) rec
fixCore1 (fun _ => arbitrary β) rec
@[inline] def fix {α β : Type u} [Inhabited β] (rec : (α → β) → α → β) : α → β :=
fixCore1 (fun _ => default β) rec
fixCore1 (fun _ => arbitrary β) rec
def bfix2 {α₁ α₂ β : Type u} (base : α₁ → α₂ → β) (rec : (α₁ → α₂ → β) → α₁ → α₂ → β) : Nat → α₁ → α₂ → β
| 0, a₁, a₂ => base a₁ a₂
@ -33,7 +33,7 @@ def fixCore2 {α₁ α₂ β : Type u} (base : α₁ → α₂ → β) (rec : (
bfix2 base rec usizeSz
@[inline] def fix2 {α₁ α₂ β : Type u} [Inhabited β] (rec : (α₁ → α₂ → β) → α₁ → α₂ → β) : α₁ → α₂ → β :=
fixCore2 (fun _ _ => default β) rec
fixCore2 (fun _ _ => arbitrary β) rec
def bfix3 {α₁ α₂ α₃ β : Type u} (base : α₁ → α₂ → α₃ → β) (rec : (α₁ → α₂ → α₃ → β) → α₁ → α₂ → α₃ → β) : Nat → α₁ → α₂ → α₃ → β
| 0, a₁, a₂, a₃ => base a₁ a₂ a₃
@ -44,7 +44,7 @@ def fixCore3 {α₁ α₂ α₃ β : Type u} (base : α₁ → α₂ → α₃
bfix3 base rec usizeSz
@[inline] def fix3 {α₁ α₂ α₃ β : Type u} [Inhabited β] (rec : (α₁ → α₂ → α₃ → β) → α₁ → α₂ → α₃ → β) : α₁ → α₂ → α₃ → β :=
fixCore3 (fun _ _ _ => default β) rec
fixCore3 (fun _ _ _ => arbitrary β) rec
def bfix4 {α₁ α₂ α₃ α₄ β : Type u} (base : α₁ → α₂ → α₃ → α₄ → β) (rec : (α₁ → α₂ → α₃ → α₄ → β) → α₁ → α₂ → α₃ → α₄ → β) : Nat → α₁ → α₂ → α₃ → α₄ → β
| 0, a₁, a₂, a₃, a₄ => base a₁ a₂ a₃ a₄
@ -55,7 +55,7 @@ def fixCore4 {α₁ α₂ α₃ α₄ β : Type u} (base : α₁ → α₂ →
bfix4 base rec usizeSz
@[inline] def fix4 {α₁ α₂ α₃ α₄ β : Type u} [Inhabited β] (rec : (α₁ → α₂ → α₃ → α₄ → β) → α₁ → α₂ → α₃ → α₄ → β) : α₁ → α₂ → α₃ → α₄ → β :=
fixCore4 (fun _ _ _ _ => default β) rec
fixCore4 (fun _ _ _ _ => arbitrary β) rec
def bfix5 {α₁ α₂ α₃ α₄ α₅ β : Type u} (base : α₁ → α₂ → α₃ → α₄ → α₅ → β) (rec : (α₁ → α₂ → α₃ → α₄ → α₅ → β) → α₁ → α₂ → α₃ → α₄ → α₅ → β) : Nat → α₁ → α₂ → α₃ → α₄ → α₅ → β
| 0, a₁, a₂, a₃, a₄, a₅ => base a₁ a₂ a₃ a₄ a₅
@ -66,7 +66,7 @@ def fixCore5 {α₁ α₂ α₃ α₄ α₅ β : Type u} (base : α₁ → α₂
bfix5 base rec usizeSz
@[inline] def fix5 {α₁ α₂ α₃ α₄ α₅ β : Type u} [Inhabited β] (rec : (α₁ → α₂ → α₃ → α₄ → α₅ → β) → α₁ → α₂ → α₃ → α₄ → α₅ → β) : α₁ → α₂ → α₃ → α₄ → α₅ → β :=
fixCore5 (fun _ _ _ _ _ => default β) rec
fixCore5 (fun _ _ _ _ _ => arbitrary β) rec
def bfix6 {α₁ α₂ α₃ α₄ α₅ α₆ β : Type u} (base : α₁ → α₂ → α₃ → α₄ → α₅ → α₆ → β) (rec : (α₁ → α₂ → α₃ → α₄ → α₅ → α₆ → β) → α₁ → α₂ → α₃ → α₄ → α₅ → α₆ → β) : Nat → α₁ → α₂ → α₃ → α₄ → α₅ → α₆ → β
| 0, a₁, a₂, a₃, a₄, a₅, a₆ => base a₁ a₂ a₃ a₄ a₅ a₆
@ -77,4 +77,4 @@ def fixCore6 {α₁ α₂ α₃ α₄ α₅ α₆ β : Type u} (base : α₁ →
bfix6 base rec usizeSz
@[inline] def fix6 {α₁ α₂ α₃ α₄ α₅ α₆ β : Type u} [Inhabited β] (rec : (α₁ → α₂ → α₃ → α₄ → α₅ → α₆ → β) → α₁ → α₂ → α₃ → α₄ → α₅ → α₆ → β) : α₁ → α₂ → α₃ → α₄ → α₅ → α₆ → β :=
fixCore6 (fun _ _ _ _ _ _ => default β) rec
fixCore6 (fun _ _ _ _ _ _ => arbitrary β) rec

2
library/Init/Lean/AbstractMetavarContext.lean
View file

@ -85,7 +85,7 @@ structure MetavarDecl :=
namespace MetavarDecl
instance : Inhabited MetavarDecl :=
⟨⟨default _, default _, default _, false⟩⟩
⟨⟨arbitrary _, arbitrary _, arbitrary _, false⟩⟩
end MetavarDecl

16
library/Init/Lean/Attributes.lean
View file

@ -26,19 +26,19 @@ structure AttributeImpl :=
(applicationTime := AttributeApplicationTime.afterTypeChecking)
instance AttributeImpl.inhabited : Inhabited AttributeImpl :=
⟨{ name := default _, descr := default _, add := fun env _ _ _ => pure env }⟩
⟨{ name := arbitrary _, descr := arbitrary _, add := fun env _ _ _ => pure env }⟩
def mkAttributeMapRef : IO (IO.Ref (HashMap Name AttributeImpl)) :=
IO.mkRef {}
@[init mkAttributeMapRef]
constant attributeMapRef : IO.Ref (HashMap Name AttributeImpl) := default _
constant attributeMapRef : IO.Ref (HashMap Name AttributeImpl) := arbitrary _
def mkAttributeArrayRef : IO (IO.Ref (Array AttributeImpl)) :=
IO.mkRef #[]
@[init mkAttributeArrayRef]
constant attributeArrayRef : IO.Ref (Array AttributeImpl) := default _
constant attributeArrayRef : IO.Ref (Array AttributeImpl) := arbitrary _
/- Low level attribute registration function. -/
def registerAttribute (attr : AttributeImpl) : IO Unit :=
@ -174,7 +174,7 @@ do ext : PersistentEnvExtension Name NameSet ← registerPersistentEnvExtension
namespace TagAttribute
instance : Inhabited TagAttribute := ⟨{attr := default _, ext := default _}⟩
instance : Inhabited TagAttribute := ⟨{attr := arbitrary _, ext := arbitrary _}⟩
def hasTag (attr : TagAttribute) (env : Environment) (decl : Name) : Bool :=
match env.getModuleIdxFor decl with
@ -225,12 +225,12 @@ do ext : PersistentEnvExtension (Name × α) (NameMap α) ← registerPersistent
namespace ParametricAttribute
instance {α : Type} : Inhabited (ParametricAttribute α) := ⟨{attr := default _, ext := default _}⟩
instance {α : Type} : Inhabited (ParametricAttribute α) := ⟨{attr := arbitrary _, ext := arbitrary _}⟩
def getParam {α : Type} [Inhabited α] (attr : ParametricAttribute α) (env : Environment) (decl : Name) : Option α :=
match env.getModuleIdxFor decl with
| some modIdx =>
match (attr.ext.getModuleEntries env modIdx).binSearch (decl, default _) (fun a b => Name.quickLt a.1 b.1) with
match (attr.ext.getModuleEntries env modIdx).binSearch (decl, arbitrary _) (fun a b => Name.quickLt a.1 b.1) with
| some (_, val) => some val
| none => none
| none => (attr.ext.getState env).find decl
@ -279,12 +279,12 @@ do ext : PersistentEnvExtension (Name × α) (NameMap α) ← registerPersistent
namespace EnumAttributes
instance {α : Type} : Inhabited (EnumAttributes α) := ⟨{attrs := [], ext := default _}⟩
instance {α : Type} : Inhabited (EnumAttributes α) := ⟨{attrs := [], ext := arbitrary _}⟩
def getValue {α : Type} [Inhabited α] (attr : EnumAttributes α) (env : Environment) (decl : Name) : Option α :=
match env.getModuleIdxFor decl with
| some modIdx =>
match (attr.ext.getModuleEntries env modIdx).binSearch (decl, default _) (fun a b => Name.quickLt a.1 b.1) with
match (attr.ext.getModuleEntries env modIdx).binSearch (decl, arbitrary _) (fun a b => Name.quickLt a.1 b.1) with
| some (_, val) => some val
| none => none
| none => (attr.ext.getState env).find decl

4
library/Init/Lean/AuxRecursor.lean
View file

@ -12,7 +12,7 @@ def mkAuxRecursorExtension : IO TagDeclarationExtension :=
mkTagDeclarationExtension `auxRec
@[init mkAuxRecursorExtension]
constant auxRecExt : TagDeclarationExtension := default _
constant auxRecExt : TagDeclarationExtension := arbitrary _
@[export lean_mark_aux_recursor]
def markAuxRecursor (env : Environment) (n : Name) : Environment :=
@ -26,7 +26,7 @@ def mkNoConfusionExtension : IO TagDeclarationExtension :=
mkTagDeclarationExtension `noConf
@[init mkNoConfusionExtension]
constant noConfusionExt : TagDeclarationExtension := default _
constant noConfusionExt : TagDeclarationExtension := arbitrary _
@[export lean_mark_no_confusion]
def markNoConfusion (env : Environment) (n : Name) : Environment :=

2
library/Init/Lean/Class.lean
View file

@ -57,7 +57,7 @@ registerSimplePersistentEnvExtension {
}
@[init mkClassExtension]
constant classExtension : SimplePersistentEnvExtension ClassEntry ClassState := default _
constant classExtension : SimplePersistentEnvExtension ClassEntry ClassState := arbitrary _
@[export lean_is_class]
def isClass (env : Environment) (n : Name) : Bool :=

2
library/Init/Lean/Compiler/ClosedTermCache.lean
View file

@ -20,7 +20,7 @@ registerSimplePersistentEnvExtension {
}
@[init mkClosedTermCacheExtension]
constant closedTermCacheExt : SimplePersistentEnvExtension (Expr × Name) ClosedTermCache := default _
constant closedTermCacheExt : SimplePersistentEnvExtension (Expr × Name) ClosedTermCache := arbitrary _
@[export lean_cache_closed_term_name]
def cacheClosedTermName (env : Environment) (e : Expr) (n : Name) : Environment :=

2
library/Init/Lean/Compiler/ExportAttr.lean
View file

@ -26,7 +26,7 @@ registerParametricAttribute `export "name to be used by code generators" $ fun _
| _ => Except.error "unexpected kind of argument"
@[init mkExportAttr]
constant exportAttr : ParametricAttribute Name := default _
constant exportAttr : ParametricAttribute Name := arbitrary _
@[export lean_get_export_name_for]
def getExportNameFor (env : Environment) (n : Name) : Option Name :=

4
library/Init/Lean/Compiler/ExternAttr.lean
View file

@ -78,7 +78,7 @@ match s with
| _ => Except.error "unexpected kind of argument"
@[extern "lean_add_extern"]
constant addExtern (env : Environment) (n : Name) : ExceptT String Id Environment := default _
constant addExtern (env : Environment) (n : Name) : ExceptT String Id Environment := arbitrary _
def mkExternAttr : IO (ParametricAttribute ExternAttrData) :=
registerParametricAttribute `extern "builtin and foreign functions"
@ -90,7 +90,7 @@ registerParametricAttribute `extern "builtin and foreign functions"
pure env)
@[init mkExternAttr]
constant externAttr : ParametricAttribute ExternAttrData := default _
constant externAttr : ParametricAttribute ExternAttrData := arbitrary _
@[export lean_get_extern_attr_data]
def getExternAttrData (env : Environment) (n : Name) : Option ExternAttrData :=

6
library/Init/Lean/Compiler/IR/Basic.lean
View file

@ -294,7 +294,7 @@ abbrev Alt := AltCore FnBody
@[matchPattern] abbrev Alt.default := @AltCore.default FnBody
instance altInh : Inhabited Alt :=
⟨Alt.default (default _)⟩
⟨Alt.default (arbitrary _)⟩
def FnBody.isTerminal : FnBody → Bool
| FnBody.case _ _ _ _ => true
@ -376,7 +376,7 @@ partial def reshapeAux : Array FnBody → Nat → FnBody → FnBody
if i == 0 then b
else
let i := i - 1;
let (curr, a) := a.swapAt! i (default _);
let (curr, a) := a.swapAt! i (arbitrary _);
let b := curr.setBody b;
reshapeAux a i b
@ -402,7 +402,7 @@ inductive Decl
namespace Decl
instance : Inhabited Decl :=
⟨fdecl (default _) (default _) IRType.irrelevant (default _)⟩
⟨fdecl (arbitrary _) (arbitrary _) IRType.irrelevant (arbitrary _)⟩
def name : Decl → FunId
| Decl.fdecl f _ _ _ => f

2
library/Init/Lean/Compiler/IR/Borrow.lean
View file

@ -126,7 +126,7 @@ ApplyParamMap.visitDecls decls map
structure BorrowInfCtx :=
(env : Environment)
(currFn : FunId := default _) -- Function being analyzed.
(currFn : FunId := arbitrary _) -- Function being analyzed.
(paramSet : IndexSet := {}) -- Set of all function parameters in scope. This is used to implement the heuristic at `ownArgsUsingParams`
structure BorrowInfState :=

10
library/Init/Lean/Compiler/IR/Boxing.lean
View file

@ -62,16 +62,16 @@ do let ps := decl.params;
if !p.ty.isScalar then pure (newVDecls, xs.push (Arg.var q.x))
else do
x ← mkFresh;
pure (newVDecls.push (FnBody.vdecl x p.ty (Expr.unbox q.x) (default _)), xs.push (Arg.var x)))
pure (newVDecls.push (FnBody.vdecl x p.ty (Expr.unbox q.x) (arbitrary _)), xs.push (Arg.var x)))
(#[], #[]);
r ← mkFresh;
let newVDecls := newVDecls.push (FnBody.vdecl r decl.resultType (Expr.fap decl.name xs) (default _));
let newVDecls := newVDecls.push (FnBody.vdecl r decl.resultType (Expr.fap decl.name xs) (arbitrary _));
body ←
if !decl.resultType.isScalar then do {
pure $ reshape newVDecls (FnBody.ret (Arg.var r))
} else do {
newR ← mkFresh;
let newVDecls := newVDecls.push (FnBody.vdecl newR IRType.object (Expr.box decl.resultType r) (default _));
let newVDecls := newVDecls.push (FnBody.vdecl newR IRType.object (Expr.box decl.resultType r) (arbitrary _));
pure $ reshape newVDecls (FnBody.ret (Arg.var newR))
};
pure $ Decl.fdecl (mkBoxedName decl.name) qs IRType.object body
@ -106,7 +106,7 @@ def eqvTypes (t₁ t₂ : IRType) : Bool :=
(t₁.isScalar == t₂.isScalar) && (!t₁.isScalar || t₁ == t₂)
structure BoxingContext :=
(f : FunId := default _) (localCtx : LocalContext := {}) (resultType : IRType := IRType.irrelevant) (decls : Array Decl) (env : Environment)
(f : FunId := arbitrary _) (localCtx : LocalContext := {}) (resultType : IRType := IRType.irrelevant) (decls : Array Decl) (env : Environment)
structure BoxingState :=
(nextIdx : Index)
@ -149,7 +149,7 @@ def getDecl (fid : FunId) : M Decl :=
do ctx ← read;
match findEnvDecl' ctx.env fid ctx.decls with
| some decl => pure decl
| none => pure (default _) -- unreachable if well-formed
| none => pure (arbitrary _) -- unreachable if well-formed
@[inline] def withParams {α : Type} (xs : Array Param) (k : M α) : M α :=
adaptReader (fun (ctx : BoxingContext) => { localCtx := ctx.localCtx.addParams xs, .. ctx }) k

2
library/Init/Lean/Compiler/IR/CompilerM.lean
View file

@ -89,7 +89,7 @@ registerSimplePersistentEnvExtension {
}
@[init mkDeclMapExtension]
constant declMapExt : SimplePersistentEnvExtension Decl DeclMap := default _
constant declMapExt : SimplePersistentEnvExtension Decl DeclMap := arbitrary _
@[export lean_ir_find_env_decl]
def findEnvDecl (env : Environment) (n : Name) : Option Decl :=

2
library/Init/Lean/Compiler/IR/CtorLayout.lean
View file

@ -36,7 +36,7 @@ structure CtorLayout :=
(scalarSize : Nat)
@[extern "lean_ir_get_ctor_layout"]
constant getCtorLayout (env : Environment) (ctorName : Name) : Except String CtorLayout := default _
constant getCtorLayout (env : Environment) (ctorName : Name) : Except String CtorLayout := arbitrary _
end IR
end Lean

2
library/Init/Lean/Compiler/IR/ElimDeadBranches.lean
View file

@ -106,7 +106,7 @@ registerSimplePersistentEnvExtension {
}
@[init mkFunctionSummariesExtension]
constant functionSummariesExt : SimplePersistentEnvExtension (FunId × Value) FunctionSummaries := default _
constant functionSummariesExt : SimplePersistentEnvExtension (FunId × Value) FunctionSummaries := arbitrary _
def addFunctionSummary (env : Environment) (fid : FunId) (v : Value) : Environment :=
functionSummariesExt.addEntry env (fid, v)

2
library/Init/Lean/Compiler/IR/EmitC.lean
View file

@ -26,7 +26,7 @@ structure Context :=
(env : Environment)
(modName : Name)
(jpMap : JPParamsMap := {})
(mainFn : FunId := default _)
(mainFn : FunId := arbitrary _)
(mainParams : Array Param := #[])
abbrev M := ReaderT Context (EStateM String String)

2
library/Init/Lean/Compiler/IR/RC.lean
View file

@ -33,7 +33,7 @@ structure Context :=
def getDecl (ctx : Context) (fid : FunId) : Decl :=
match findEnvDecl' ctx.env fid ctx.decls with
| some decl => decl
| none => default _ -- unreachable if well-formed
| none => arbitrary _ -- unreachable if well-formed
def getVarInfo (ctx : Context) (x : VarId) : VarInfo :=
match ctx.varMap.find x with

2
library/Init/Lean/Compiler/IR/UnboxResult.lean
View file

@ -23,7 +23,7 @@ registerTagAttribute `unbox "compiler tries to unbox result values if their type
| _ => Except.error "constant must be an inductive type"
@[init mkUnboxAttr]
constant unboxAttr : TagAttribute := default _
constant unboxAttr : TagAttribute := arbitrary _
def hasUnboxAttr (env : Environment) (n : Name) : Bool :=
unboxAttr.hasTag env n

2
library/Init/Lean/Compiler/ImplementedByAttr.lean
View file

@ -24,7 +24,7 @@ registerParametricAttribute `implementedBy "name of the Lean (probably unsafe) f
| _ => Except.error "expected identifier"
@[init mkImplementedByAttr]
constant implementedByAttr : ParametricAttribute Name := default _
constant implementedByAttr : ParametricAttribute Name := arbitrary _
@[export lean_get_implemented_by]
def getImplementedBy (env : Environment) (n : Name) : Option Name :=

2
library/Init/Lean/Compiler/InitAttr.lean
View file

@ -44,7 +44,7 @@ registerParametricAttribute `init "initialization procedure for global reference
| _ => Except.error "unexpected kind of argument"
@[init mkInitAttr]
constant initAttr : ParametricAttribute Name := default _
constant initAttr : ParametricAttribute Name := arbitrary _
def isIOUnitInitFn (env : Environment) (fn : Name) : Bool :=
match initAttr.getParam env fn with

2
library/Init/Lean/Compiler/InlineAttrs.lean
View file

@ -37,7 +37,7 @@ registerEnumAttributes `inlineAttrs
(fun env declName _ => checkIsDefinition env declName)
@[init mkInlineAttrs]
constant inlineAttrs : EnumAttributes InlineAttributeKind := default _
constant inlineAttrs : EnumAttributes InlineAttributeKind := arbitrary _
private partial def hasInlineAttrAux (env : Environment) (kind : InlineAttributeKind) : Name → Bool
| n =>

2
library/Init/Lean/Compiler/NeverExtractAttr.lean
View file

@ -13,7 +13,7 @@ def mkNeverExtractAttr : IO TagAttribute :=
registerTagAttribute `neverExtract "instruct the compiler that function applications using the tagged declaration should not be extracted when they are closed terms, nor common subexpression should be performed. This is useful for declarations that have implicit effects."
@[init mkNeverExtractAttr]
constant neverExtractAttr : TagAttribute := default _
constant neverExtractAttr : TagAttribute := arbitrary _
private partial def hasNeverExtractAttributeAux (env : Environment) : Name → Bool
| n =>

4
library/Init/Lean/Compiler/Specialize.lean
View file

@ -33,7 +33,7 @@ registerEnumAttributes `specializeAttrs
(fun env declName _ => checkIsDefinition env declName)
@[init mkSpecializeAttrs]
constant specializeAttrs : EnumAttributes SpecializeAttributeKind := default _
constant specializeAttrs : EnumAttributes SpecializeAttributeKind := arbitrary _
private partial def hasSpecializeAttrAux (env : Environment) (kind : SpecializeAttributeKind) : Name → Bool
| n => match specializeAttrs.getValue env n with
@ -88,7 +88,7 @@ registerSimplePersistentEnvExtension {
}
@[init mkSpecExtension]
constant specExtension : SimplePersistentEnvExtension SpecEntry SpecState := default _
constant specExtension : SimplePersistentEnvExtension SpecEntry SpecState := arbitrary _
@[export lean_add_specialization_info]
def addSpecializationInfo (env : Environment) (fn : Name) (info : SpecInfo) : Environment :=

4
library/Init/Lean/Declaration.lean
View file

@ -181,10 +181,10 @@ def hints : ConstantInfo → ReducibilityHints
| _ => ReducibilityHints.opaque
@[extern "lean_instantiate_type_lparams"]
constant instantiateTypeLevelParams (c : ConstantInfo) (ls : List Level) : Expr := default _
constant instantiateTypeLevelParams (c : ConstantInfo) (ls : List Level) : Expr := arbitrary _
@[extern "lean_instantiate_value_lparams"]
constant instantiateValueLevelParams (c : ConstantInfo) (ls : List Level) : Expr := default _
constant instantiateValueLevelParams (c : ConstantInfo) (ls : List Level) : Expr := arbitrary _
end ConstantInfo
end Lean

2
library/Init/Lean/Elaborator/Alias.lean
View file

@ -26,7 +26,7 @@ registerSimplePersistentEnvExtension {
}
@[init mkAliasExtension]
constant aliasExtension : SimplePersistentEnvExtension AliasEntry AliasState := default _
constant aliasExtension : SimplePersistentEnvExtension AliasEntry AliasState := arbitrary _
/- Add alias `a` for `e` -/
def addAlias (env : Environment) (a : Name) (e : Name) : Environment :=

18
library/Init/Lean/Elaborator/Basic.lean
View file

@ -43,7 +43,7 @@ structure ElabScope :=
namespace ElabScope
instance : Inhabited ElabScope := ⟨{ cmd := "", header := default _ }⟩
instance : Inhabited ElabScope := ⟨{ cmd := "", header := arbitrary _ }⟩
end ElabScope
@ -83,9 +83,9 @@ abbrev CommandElabTable : Type := SMap SyntaxNodeKind CommandElab
def mkBuiltinTermElabTable : IO (IO.Ref TermElabTable) := IO.mkRef {}
def mkBuiltinCommandElabTable : IO (IO.Ref CommandElabTable) := IO.mkRef {}
@[init mkBuiltinTermElabTable]
constant builtinTermElabTable : IO.Ref TermElabTable := default _
constant builtinTermElabTable : IO.Ref TermElabTable := arbitrary _
@[init mkBuiltinCommandElabTable]
constant builtinCommandElabTable : IO.Ref CommandElabTable := default _
constant builtinCommandElabTable : IO.Ref CommandElabTable := arbitrary _
def addBuiltinTermElab (k : SyntaxNodeKind) (declName : Name) (elab : TermElab) : IO Unit :=
do m ← builtinTermElabTable.get;
@ -181,7 +181,7 @@ structure ElabAttribute (σ : Type) :=
namespace ElabAttribute
instance {σ} [Inhabited σ] : Inhabited (ElabAttribute σ) := ⟨{ attr := default _, ext := default _, kind := "" }⟩
instance {σ} [Inhabited σ] : Inhabited (ElabAttribute σ) := ⟨{ attr := arbitrary _, ext := arbitrary _, kind := "" }⟩
end ElabAttribute
@ -213,13 +213,13 @@ abbrev TermElabAttribute := ElabAttribute TermElabTable
def mkTermElabAttribute : IO TermElabAttribute :=
mkElabAttribute `elabTerm "term" builtinTermElabTable
@[init mkTermElabAttribute]
constant termElabAttribute : TermElabAttribute := default _
constant termElabAttribute : TermElabAttribute := arbitrary _
abbrev CommandElabAttribute := ElabAttribute CommandElabTable
def mkCommandElabAttribute : IO CommandElabAttribute :=
mkElabAttribute `commandTerm "command" builtinCommandElabTable
@[init mkCommandElabAttribute]
constant commandElabAttribute : CommandElabAttribute := default _
constant commandElabAttribute : CommandElabAttribute := arbitrary _
namespace Elab
def logMessage (msg : Message) : Elab Unit :=
@ -398,7 +398,7 @@ do env ← mkEmptyEnvironment;
| EStateM.Result.error _ s => pure (s.elabState.env, s.elabState.messages)
instance {α} : Inhabited (Elab α) :=
⟨fun _ => default _⟩
⟨fun _ => arbitrary _⟩
def mkFreshName : Elab Name :=
modifyGet $ fun s => (s.ngen.curr, { ngen := s.ngen.next, .. s })
@ -431,7 +431,7 @@ modifyGet $ fun s =>
| { scopes := h::t, .. } =>
let (a, h) := f h;
(a, { scopes := h :: t, .. s })
| _ => (default _, s)
| _ => (arbitrary _, s)
def localContext : Elab LocalContext :=
do scope ← getScope; pure scope.lctx
@ -515,7 +515,7 @@ match unsafeIO x with
| Except.error e => throw (ElabException.io e)
@[implementedBy runIOUnsafe]
constant runIO {α : Type} (x : IO α) : Elab α := default _
constant runIO {α : Type} (x : IO α) : Elab α := arbitrary _
end Elab

2
library/Init/Lean/Elaborator/ElabStrategyAttrs.lean
View file

@ -25,7 +25,7 @@ registerEnumAttributes `elaboratorStrategy
(`elabAsEliminator, "instructs elaborator that the arguments of the function application (f ...) should be elaborated as f were an eliminator", ElaboratorStrategy.asEliminator)]
@[init mkElaboratorStrategyAttrs]
constant elaboratorStrategyAttrs : EnumAttributes ElaboratorStrategy := default _
constant elaboratorStrategyAttrs : EnumAttributes ElaboratorStrategy := arbitrary _
@[export lean_get_elaborator_strategy]
def getElaboratorStrategy (env : Environment) (n : Name) : Option ElaboratorStrategy :=

4
library/Init/Lean/Elaborator/PreTerm.lean
View file

@ -11,7 +11,7 @@ namespace Lean
abbrev PreTerm := Expr
@[extern "lean_old_elaborate"]
constant oldElaborateAux : Environment → Options → MetavarContext → LocalContext → PreTerm → Except (Option Position × Format) (Environment × MetavarContext × Expr) := default _
constant oldElaborateAux : Environment → Options → MetavarContext → LocalContext → PreTerm → Except (Option Position × Format) (Environment × MetavarContext × Expr) := arbitrary _
abbrev PreTermElab := SyntaxNode Expr → Elab PreTerm
@ -20,7 +20,7 @@ abbrev PreTermElabTable : Type := HashMap SyntaxNodeKind PreTermElab
def mkBuiltinPreTermElabTable : IO (IO.Ref PreTermElabTable) := IO.mkRef {}
@[init mkBuiltinPreTermElabTable]
constant builtinPreTermElabTable : IO.Ref PreTermElabTable := default _
constant builtinPreTermElabTable : IO.Ref PreTermElabTable := arbitrary _
def addBuiltinPreTermElab (k : SyntaxNodeKind) (declName : Name) (elab : PreTermElab) : IO Unit :=
do m ← builtinPreTermElabTable.get;

44
library/Init/Lean/Environment.lean
View file

@ -30,7 +30,7 @@ abbrev ConstMap := SMap Name ConstantInfo
structure EnvironmentHeader :=
(trustLevel : UInt32 := 0)
(quotInit : Bool := false)
(mainModule : Name := default _)
(mainModule : Name := arbitrary _)
(imports : Array Name := #[])
/- TODO: mark opaque. -/
@ -107,11 +107,11 @@ namespace Environment
/- Type check given declaration and add it to the environment -/
@[extern "lean_add_decl"]
constant addDecl (env : Environment) (decl : @& Declaration) : Except KernelException Environment := default _
constant addDecl (env : Environment) (decl : @& Declaration) : Except KernelException Environment := arbitrary _
/- Compile the given declaration, it assumes the declaration has already been added to the environment using `addDecl`. -/
@[extern "lean_compile_decl"]
constant compileDecl (env : Environment) (opt : @& Options) (decl : @& Declaration) : Except KernelException Environment := default _
constant compileDecl (env : Environment) (opt : @& Options) (decl : @& Declaration) : Except KernelException Environment := arbitrary _
def addAndCompile (env : Environment) (opt : Options) (decl : Declaration) : Except KernelException Environment :=
do env ← addDecl env decl;
@ -131,7 +131,7 @@ unsafe def setStateUnsafe {σ : Type} (ext : EnvExtension σ) (env : Environment
{ extensions := env.extensions.set! ext.idx (unsafeCast s), .. env }
@[implementedBy setStateUnsafe]
constant setState {σ : Type} (ext : EnvExtension σ) (env : Environment) (s : σ) : Environment := default _
constant setState {σ : Type} (ext : EnvExtension σ) (env : Environment) (s : σ) : Environment := arbitrary _
unsafe def getStateUnsafe {σ : Type} (ext : EnvExtension σ) (env : Environment) : σ :=
let s : EnvExtensionState := env.extensions.get! ext.idx;
@ -148,7 +148,7 @@ constant getState {σ : Type} (ext : EnvExtension σ) (env : Environment) : σ :
.. env }
@[implementedBy modifyStateUnsafe]
constant modifyState {σ : Type} (ext : EnvExtension σ) (env : Environment) (f : σ → σ) : Environment := default _
constant modifyState {σ : Type} (ext : EnvExtension σ) (env : Environment) (f : σ → σ) : Environment := arbitrary _
end EnvExtension
@ -156,10 +156,10 @@ private def mkEnvExtensionsRef : IO (IO.Ref (Array (EnvExtension EnvExtensionSta
IO.mkRef #[]
@[init mkEnvExtensionsRef]
private constant envExtensionsRef : IO.Ref (Array (EnvExtension EnvExtensionState)) := default _
private constant envExtensionsRef : IO.Ref (Array (EnvExtension EnvExtensionState)) := arbitrary _
instance EnvExtension.Inhabited (σ : Type) [Inhabited σ] : Inhabited (EnvExtension σ) :=
⟨{ idx := 0, stateInh := default _, mkInitial := default _ }⟩
⟨{ idx := 0, stateInh := arbitrary _, mkInitial := arbitrary _ }⟩
unsafe def registerEnvExtensionUnsafe {σ : Type} [Inhabited σ] (mkInitial : IO σ) : IO (EnvExtension σ) :=
do initializing ← IO.initializing;
@ -169,7 +169,7 @@ do initializing ← IO.initializing;
let ext : EnvExtension σ := {
idx := idx,
mkInitial := mkInitial,
stateInh := default _
stateInh := arbitrary _
};
envExtensionsRef.modify (fun exts => exts.push (unsafeCast ext));
pure ext
@ -179,7 +179,7 @@ do initializing ← IO.initializing;
1- Our implementation assumes the number of extensions does not change after an environment object is created.
2- We do not use any synchronization primitive to access `envExtensionsRef`. -/
@[implementedBy registerEnvExtensionUnsafe]
constant registerEnvExtension {σ : Type} [Inhabited σ] (mkInitial : IO σ) : IO (EnvExtension σ) := default _
constant registerEnvExtension {σ : Type} [Inhabited σ] (mkInitial : IO σ) : IO (EnvExtension σ) := arbitrary _
private def mkInitialExtensionStates : IO (Array EnvExtensionState) :=
do exts ← envExtensionsRef.get; exts.mapM $ fun ext => ext.mkInitial
@ -217,12 +217,12 @@ def EnvExtensionEntry := NonScalar
instance EnvExtensionEntry.inhabited : Inhabited EnvExtensionEntry := inferInstanceAs (Inhabited NonScalar)
instance PersistentEnvExtensionState.inhabited {α σ} [Inhabited σ] : Inhabited (PersistentEnvExtensionState α σ) :=
⟨{importedEntries := #[], state := default _ }⟩
⟨{importedEntries := #[], state := arbitrary _ }⟩
instance PersistentEnvExtension.inhabited {α σ} [Inhabited σ] : Inhabited (PersistentEnvExtension α σ) :=
⟨{ toEnvExtension := { idx := 0, stateInh := default _, mkInitial := default _ },
name := default _,
addImportedFn := fun _ => default _,
⟨{ toEnvExtension := { idx := 0, stateInh := arbitrary _, mkInitial := arbitrary _ },
name := arbitrary _,
addImportedFn := fun _ => arbitrary _,
addEntryFn := fun s _ => s,
exportEntriesFn := fun _ => #[],
statsFn := fun _ => Format.nil }⟩
@ -252,7 +252,7 @@ private def mkPersistentEnvExtensionsRef : IO (IO.Ref (Array (PersistentEnvExten
IO.mkRef #[]
@[init mkPersistentEnvExtensionsRef]
private constant persistentEnvExtensionsRef : IO.Ref (Array (PersistentEnvExtension EnvExtensionEntry EnvExtensionState)) := default _
private constant persistentEnvExtensionsRef : IO.Ref (Array (PersistentEnvExtension EnvExtensionEntry EnvExtensionState)) := arbitrary _
structure PersistentEnvExtensionDescr (α σ : Type) :=
(name : Name)
@ -283,7 +283,7 @@ do pExts ← persistentEnvExtensionsRef.get;
pure pExt
@[implementedBy registerPersistentEnvExtensionUnsafe]
constant registerPersistentEnvExtension {α σ : Type} [Inhabited σ] (descr : PersistentEnvExtensionDescr α σ) : IO (PersistentEnvExtension α σ) := default _
constant registerPersistentEnvExtension {α σ : Type} [Inhabited σ] (descr : PersistentEnvExtensionDescr α σ) : IO (PersistentEnvExtension α σ) := arbitrary _
/- Simple PersistentEnvExtension that implements exportEntriesFn using a list of entries. -/
@ -395,7 +395,7 @@ def regModListExtension : IO (EnvExtension (List Modification)) :=
registerEnvExtension (pure [])
@[init regModListExtension]
constant modListExtension : EnvExtension (List Modification) := default _
constant modListExtension : EnvExtension (List Modification) := arbitrary _
/- The C++ code uses this function to store the given modification object into the environment. -/
@[export lean_environment_add_modification]
@ -405,10 +405,10 @@ modListExtension.modifyState env $ fun mods => mod :: mods
/- mkModuleData invokes this function to convert a list of modification objects into
a serialized byte array. -/
@[extern 2 "lean_serialize_modifications"]
constant serializeModifications : List Modification → IO ByteArray := default _
constant serializeModifications : List Modification → IO ByteArray := arbitrary _
@[extern 3 "lean_perform_serialized_modifications"]
constant performModifications : Environment → ByteArray → IO Environment := default _
constant performModifications : Environment → ByteArray → IO Environment := arbitrary _
/- Content of a .olean file.
We use `compact.cpp` to generate the image of this object in disk. -/
@ -419,12 +419,12 @@ structure ModuleData :=
(serialized : ByteArray) -- Legacy support: serialized modification objects
instance ModuleData.inhabited : Inhabited ModuleData :=
⟨{imports := default _, constants := default _, entries := default _, serialized := default _}⟩
⟨{imports := arbitrary _, constants := arbitrary _, entries := arbitrary _, serialized := arbitrary _}⟩
@[extern 3 "lean_save_module_data"]
constant saveModuleData (fname : @& String) (m : ModuleData) : IO Unit := default _
constant saveModuleData (fname : @& String) (m : ModuleData) : IO Unit := arbitrary _
@[extern 2 "lean_read_module_data"]
constant readModuleData (fname : @& String) : IO ModuleData := default _
constant readModuleData (fname : @& String) : IO ModuleData := arbitrary _
def mkModuleData (env : Environment) : IO ModuleData :=
do pExts ← persistentEnvExtensionsRef.get;
@ -520,7 +520,7 @@ registerSimplePersistentEnvExtension {
}
@[init regNamespacesExtension]
constant namespacesExt : SimplePersistentEnvExtension Name NameSet := default _
constant namespacesExt : SimplePersistentEnvExtension Name NameSet := arbitrary _
def registerNamespace (env : Environment) (n : Name) : Environment :=
if (namespacesExt.getState env).contains n then env else namespacesExt.addEntry env n

2
library/Init/Lean/EqnCompiler/MatchPattern.lean
View file

@ -13,7 +13,7 @@ def mkMatchPatternAttr : IO TagAttribute :=
registerTagAttribute `matchPattern "mark that a definition can be used in a pattern (remark: the dependent pattern matching compiler will unfold the definition)"
@[init mkMatchPatternAttr]
constant matchPatternAttr : TagAttribute := default _
constant matchPatternAttr : TagAttribute := arbitrary _
@[export lean_has_match_pattern_attribute]
def hasMatchPatternAttribute (env : Environment) (n : Name) : Bool :=

36
library/Init/Lean/Expr.lean
View file

@ -82,7 +82,7 @@ attribute [extern "lean_expr_mk_proj"] Expr.proj
-- deprecated Constructor
@[extern "lean_expr_local"]
constant Expr.local (n : Name) (pp : Name) (ty : Expr) (bi : BinderInfo) : Expr := default _
constant Expr.local (n : Name) (pp : Name) (ty : Expr) (bi : BinderInfo) : Expr := arbitrary _
def mkApp (f : Expr) (args : Array Expr) : Expr :=
args.foldl Expr.app f
@ -102,43 +102,43 @@ revArgs.foldr (fun a r => Expr.app r a) fn
namespace Expr
@[extern "lean_expr_hash"]
constant hash (n : @& Expr) : USize := default USize
constant hash (n : @& Expr) : USize := arbitrary USize
instance : Hashable Expr := ⟨Expr.hash⟩
-- TODO: implement it in Lean
@[extern "lean_expr_dbg_to_string"]
constant dbgToString (e : @& Expr) : String := default String
constant dbgToString (e : @& Expr) : String := arbitrary String
@[extern "lean_expr_quick_lt"]
constant quickLt (a : @& Expr) (b : @& Expr) : Bool := default _
constant quickLt (a : @& Expr) (b : @& Expr) : Bool := arbitrary _
@[extern "lean_expr_lt"]
constant lt (a : @& Expr) (b : @& Expr) : Bool := default _
constant lt (a : @& Expr) (b : @& Expr) : Bool := arbitrary _
/- Return true iff `a` and `b` are alpha equivalent.
Binder annotations are ignored. -/
@[extern "lean_expr_eqv"]
constant eqv (a : @& Expr) (b : @& Expr) : Bool := default _
constant eqv (a : @& Expr) (b : @& Expr) : Bool := arbitrary _
instance : HasBeq Expr := ⟨Expr.eqv⟩
/- Return true iff `a` and `b` are equal.
Binder names and annotations are taking into account. -/
@[extern "lean_expr_equal"]
constant equal (a : @& Expr) (b : @& Expr) : Bool := default _
constant equal (a : @& Expr) (b : @& Expr) : Bool := arbitrary _
@[extern "lean_expr_has_expr_mvar"]
constant hasExprMVar (a : @& Expr) : Bool := default _
constant hasExprMVar (a : @& Expr) : Bool := arbitrary _
@[extern "lean_expr_has_level_mvar"]
constant hasLevelMVar (a : @& Expr) : Bool := default _
constant hasLevelMVar (a : @& Expr) : Bool := arbitrary _
@[inline] def hasMVar (a : Expr) : Bool :=
a.hasExprMVar || a.hasLevelMVar
@[extern "lean_expr_has_fvar"]
constant hasFVar (a : @& Expr) : Bool := default _
constant hasFVar (a : @& Expr) : Bool := arbitrary _
def isSort : Expr → Bool
| sort _ => true
@ -308,30 +308,30 @@ def letName! : Expr → Name
/-- Instantiate the loose bound variables in `e` using `subst`.
That is, a loose `Expr.bvar i` is replaced with `subst[i]`. -/
@[extern "lean_expr_instantiate"]
constant instantiate (e : @& Expr) (subst : @& Array Expr) : Expr := default _
constant instantiate (e : @& Expr) (subst : @& Array Expr) : Expr := arbitrary _
@[extern "lean_expr_instantiate1"]
constant instantiate1 (e : @& Expr) (subst : @& Expr) : Expr := default _
constant instantiate1 (e : @& Expr) (subst : @& Expr) : Expr := arbitrary _
/-- Similar to instantiate, but `Expr.bvar i` is replaced with `subst[subst.size - i - 1]` -/
@[extern "lean_expr_instantiate_rev"]
constant instantiateRev (e : @& Expr) (subst : @& Array Expr) : Expr := default _
constant instantiateRev (e : @& Expr) (subst : @& Array Expr) : Expr := arbitrary _
/-- Similar to `instantiate`, but consider only the variables `xs` in the range `[beginIdx, endIdx)`.
Function panics if `beginIdx <= endIdx <= xs.size` does not hold. -/
@[extern "lean_expr_instantiate_range"]
constant instantiateRange (e : @& Expr) (beginIdx endIdx : @& Nat) (xs : Array Expr) : Expr := default _
constant instantiateRange (e : @& Expr) (beginIdx endIdx : @& Nat) (xs : Array Expr) : Expr := arbitrary _
/-- Replace free variables `xs` with loose bound variables. -/
@[extern "lean_expr_abstract"]
constant abstract (e : @& Expr) (xs : @& Array Expr) : Expr := default _
constant abstract (e : @& Expr) (xs : @& Array Expr) : Expr := arbitrary _
/-- Similar to `abstract`, but consider only the first `min n xs.size` entries in `xs`. -/
@[extern "lean_expr_abstract_range"]
constant abstractRange (e : @& Expr) (n : @& Nat) (xs : @& Array Expr) : Expr := default _
constant abstractRange (e : @& Expr) (n : @& Nat) (xs : @& Array Expr) : Expr := arbitrary _
@[extern "lean_instantiate_lparams"]
constant instantiateLevelParams (e : Expr) (paramNames : List Name) (lvls : List Level) : Expr := default _
constant instantiateLevelParams (e : Expr) (paramNames : List Name) (lvls : List Level) : Expr := arbitrary _
instance : HasToString Expr :=
⟨Expr.dbgToString⟩
@ -377,7 +377,7 @@ protected def beq : ExprStructEq → ExprStructEq → Bool
protected def hash : ExprStructEq → USize
| ⟨e⟩ => e.hash
instance : Inhabited ExprStructEq := ⟨{ val := default _ }⟩
instance : Inhabited ExprStructEq := ⟨{ val := arbitrary _ }⟩
instance : HasBeq ExprStructEq := ⟨ExprStructEq.beq⟩
instance : Hashable ExprStructEq := ⟨ExprStructEq.hash⟩
instance : HasToString ExprStructEq := ⟨fun e => toString e.val⟩

4
library/Init/Lean/Level.lean
View file

@ -144,12 +144,12 @@ def instantiate (s : Name → Option Level) : Level → Level
| l => l
@[extern "lean_level_hash"]
protected constant hash (n : @& Level) : USize := default USize
protected constant hash (n : @& Level) : USize := arbitrary USize
instance hashable : Hashable Level := ⟨Level.hash⟩
@[extern "lean_level_eq"]
protected constant beq (a : @& Level) (b : @& Level) : Bool := default _
protected constant beq (a : @& Level) (b : @& Level) : Bool := arbitrary _
instance : HasBeq Level := ⟨Level.beq⟩

2
library/Init/Lean/LocalContext.lean
View file

@ -15,7 +15,7 @@ inductive LocalDecl
| ldecl (index : Nat) (name : Name) (userName : Name) (type : Expr) (value : Expr)
namespace LocalDecl
instance : Inhabited LocalDecl := ⟨ldecl (default _) (default _) (default _) (default _) (default _)⟩
instance : Inhabited LocalDecl := ⟨ldecl (arbitrary _) (arbitrary _) (arbitrary _) (arbitrary _) (arbitrary _)⟩
def isLet : LocalDecl → Bool
| cdecl _ _ _ _ _ => false

4
library/Init/Lean/Message.lean
View file

@ -40,7 +40,7 @@ inductive MessageData
namespace MessageData
instance : Inhabited MessageData := ⟨MessageData.ofFormat (default _)⟩
instance : Inhabited MessageData := ⟨MessageData.ofFormat (arbitrary _)⟩
partial def formatAux : Option (Environment × MetavarContext × LocalContext) → MessageData → Format
| _, ofFormat fmt => fmt
@ -84,7 +84,7 @@ mkErrorStringWithPos msg.fileName msg.pos.line msg.pos.column
(if msg.caption == "" then "" else msg.caption ++ ":\n") ++ toString (fmt msg.data))
instance : Inhabited Message :=
⟨{ fileName := "", pos := ⟨0, 1⟩, data := default _}⟩
⟨{ fileName := "", pos := ⟨0, 1⟩, data := arbitrary _}⟩
instance : HasToString Message :=
⟨Message.toString⟩

4
library/Init/Lean/Modifiers.lean
View file

@ -12,7 +12,7 @@ def mkProtectedExtension : IO TagDeclarationExtension :=
mkTagDeclarationExtension `protected
@[init mkProtectedExtension]
constant protectedExt : TagDeclarationExtension := default _
constant protectedExt : TagDeclarationExtension := arbitrary _
@[export lean_add_protected]
def addProtected (env : Environment) (n : Name) : Environment :=
@ -26,7 +26,7 @@ def mkPrivateExtension : IO (EnvExtension Nat) :=
registerEnvExtension (pure 1)
@[init mkPrivateExtension]
constant privateExt : EnvExtension Nat := default _
constant privateExt : EnvExtension Nat := arbitrary _
/- Private name support.

2
library/Init/Lean/Name.lean
View file

@ -38,7 +38,7 @@ instance stringToName : HasCoe String Name :=
namespace Name
@[extern "lean_name_hash_usize"]
constant hash (n : @& Name) : USize := default _
constant hash (n : @& Name) : USize := arbitrary _
instance : Hashable Name :=
⟨Name.hash⟩

2
library/Init/Lean/Options.lean
View file

@ -28,7 +28,7 @@ private def initOptionDeclsRef : IO (IO.Ref OptionDecls) :=
IO.mkRef (mkNameMap OptionDecl)
@[init initOptionDeclsRef]
private constant optionDeclsRef : IO.Ref OptionDecls := default _
private constant optionDeclsRef : IO.Ref OptionDecls := arbitrary _
def registerOption (name : Name) (decl : OptionDecl) : IO Unit :=
do decls ← optionDeclsRef.get;

4
library/Init/Lean/Parser/Command.lean
View file

@ -10,7 +10,7 @@ namespace Lean
namespace Parser
@[init mkBuiltinParsingTablesRef]
constant builtinCommandParsingTable : IO.Ref ParsingTables := default _
constant builtinCommandParsingTable : IO.Ref ParsingTables := arbitrary _
@[init] def regBuiltinCommandParserAttr : IO Unit :=
registerBuiltinParserAttribute `builtinCommandParser `Lean.Parser.builtinCommandParsingTable
@ -19,7 +19,7 @@ def mkCommandParserAttribute : IO ParserAttribute :=
registerParserAttribute `commandParser "command" "command parser" (some builtinCommandParsingTable)
@[init mkCommandParserAttribute]
constant commandParserAttribute : ParserAttribute := default _
constant commandParserAttribute : ParserAttribute := arbitrary _
@[inline] def commandParser {k : ParserKind} (rbp : Nat := 0) : Parser k :=
{ fn := fun _ => commandParserAttribute.runParser rbp }

4
library/Init/Lean/Parser/Level.lean
View file

@ -10,7 +10,7 @@ namespace Lean
namespace Parser
@[init mkBuiltinParsingTablesRef]
constant builtinLevelParsingTable : IO.Ref ParsingTables := default _
constant builtinLevelParsingTable : IO.Ref ParsingTables := arbitrary _
@[init] def regBuiltinLevelParserAttr : IO Unit :=
registerBuiltinParserAttribute `builtinLevelParser `Lean.Parser.builtinLevelParsingTable
@ -19,7 +19,7 @@ def mkLevelParserAttribute : IO ParserAttribute :=
registerParserAttribute `levelParser "level" "universe level parser" (some builtinLevelParsingTable)
@[init mkLevelParserAttribute]
constant levelParserAttribute : ParserAttribute := default _
constant levelParserAttribute : ParserAttribute := arbitrary _
@[inline] def levelParser {k : ParserKind} (rbp : Nat := 0) : Parser k :=
{ fn := fun _ => levelParserAttribute.runParser rbp }

14
library/Init/Lean/Parser/Parser.lean
View file

@ -77,7 +77,7 @@ structure ParserContextCore :=
(tokens : TokenTable)
instance ParserContextCore.inhabited : Inhabited ParserContextCore :=
⟨{ input := "", fileName := "", fileMap := default _, tokens := {} }⟩
⟨{ input := "", fileName := "", fileMap := arbitrary _, tokens := {} }⟩
structure ParserContext extends ParserContextCore :=
(env : Environment)
@ -1327,7 +1327,7 @@ def mkBuiltinTokenTable : IO (IO.Ref TokenTable) :=
IO.mkRef {}
@[init mkBuiltinTokenTable]
constant builtinTokenTable : IO.Ref TokenTable := default _
constant builtinTokenTable : IO.Ref TokenTable := arbitrary _
def mkImportedTokenTable (es : Array (Array TokenConfig)) : IO TokenTable :=
do table ← builtinTokenTable.get;
@ -1341,7 +1341,7 @@ structure TokenTableAttribute :=
(attr : AttributeImpl)
(ext : PersistentEnvExtension TokenConfig TokenTable)
instance TokenTableAttribute.inhabited : Inhabited TokenTableAttribute := ⟨{ attr := default _, ext := default _ }⟩
instance TokenTableAttribute.inhabited : Inhabited TokenTableAttribute := ⟨{ attr := arbitrary _, ext := arbitrary _ }⟩
section
set_option compiler.extract_closed false
@ -1362,12 +1362,12 @@ do ext : PersistentEnvExtension TokenConfig TokenTable ← registerPersistentEnv
end
@[init mkTokenTableAttribute]
constant tokenTableAttribute : TokenTableAttribute := default _
constant tokenTableAttribute : TokenTableAttribute := arbitrary _
/- Global table with all SyntaxNodeKind's -/
def mkSyntaxNodeKindSetRef : IO (IO.Ref SyntaxNodeKindSet) := IO.mkRef {}
@[init mkSyntaxNodeKindSetRef]
constant syntaxNodeKindSetRef : IO.Ref SyntaxNodeKindSet := default _
constant syntaxNodeKindSetRef : IO.Ref SyntaxNodeKindSet := arbitrary _
def updateSyntaxNodeKinds (pinfo : ParserInfo) : IO Unit :=
syntaxNodeKindSetRef.modify pinfo.updateKindSet
@ -1487,7 +1487,7 @@ match unsafeIO (do tables ← ref.get; pure $ prattParser kind tables a c s) wit
| _ => s.mkError "failed to access builtin reference"
@[implementedBy runBuiltinParserUnsafe]
constant runBuiltinParser (kind : String) (ref : IO.Ref ParsingTables) : ParserFn leading := default _
constant runBuiltinParser (kind : String) (ref : IO.Ref ParsingTables) : ParserFn leading := arbitrary _
inductive ParserAttributeEntry
| leading (n : Name)
@ -1498,7 +1498,7 @@ structure ParserAttribute :=
(ext : PersistentEnvExtension ParserAttributeEntry ParsingTables)
(kind : String)
instance ParserAttribute.inhabited : Inhabited ParserAttribute := ⟨{ attr := default _, ext := default _, kind := "" }⟩
instance ParserAttribute.inhabited : Inhabited ParserAttribute := ⟨{ attr := arbitrary _, ext := arbitrary _, kind := "" }⟩
/-
This is just the basic skeleton where we create an

4
library/Init/Lean/Parser/Term.lean
View file

@ -11,7 +11,7 @@ namespace Lean
namespace Parser
@[init mkBuiltinParsingTablesRef]
constant builtinTermParsingTable : IO.Ref ParsingTables := default _
constant builtinTermParsingTable : IO.Ref ParsingTables := arbitrary _
@[init] def regBuiltinTermParserAttr : IO Unit :=
registerBuiltinParserAttribute `builtinTermParser `Lean.Parser.builtinTermParsingTable
@ -20,7 +20,7 @@ def mkTermParserAttribute : IO ParserAttribute :=
registerParserAttribute `termParser "term" "term parser" (some builtinTermParsingTable)
@[init mkTermParserAttribute]
constant termParserAttribute : ParserAttribute := default _
constant termParserAttribute : ParserAttribute := arbitrary _
@[inline] def termParser {k : ParserKind} (rbp : Nat := 0) : Parser k :=
{ fn := fun _ => termParserAttribute.runParser rbp }

2
library/Init/Lean/Path.lean
View file

@ -23,7 +23,7 @@ do curr ← realPathNormalized ".";
IO.mkRef #[curr]
@[init mkSearchPathRef]
constant searchPathRef : IO.Ref (Array String) := default _
constant searchPathRef : IO.Ref (Array String) := arbitrary _
def setSearchPath (s : List String) : IO Unit :=
do s ← s.mapM realPathNormalized;

8
library/Init/Lean/ProjFns.lean
View file

@ -17,7 +17,7 @@ structure ProjectionFunctionInfo :=
(fromClass : Bool) -- `true` if the structure is a class
instance ProjectionFunctionInfo.inhabited : Inhabited ProjectionFunctionInfo :=
⟨{ ctorName := default _, nparams := default _, i := 0, fromClass := false }⟩
⟨{ ctorName := arbitrary _, nparams := arbitrary _, i := 0, fromClass := false }⟩
def mkProjectionFnInfoExtension : IO (SimplePersistentEnvExtension (Name × ProjectionFunctionInfo) (NameMap ProjectionFunctionInfo)) :=
registerSimplePersistentEnvExtension {
@ -28,7 +28,7 @@ registerSimplePersistentEnvExtension {
}
@[init mkProjectionFnInfoExtension]
constant projectionFnInfoExt : SimplePersistentEnvExtension (Name × ProjectionFunctionInfo) (NameMap ProjectionFunctionInfo) := default _
constant projectionFnInfoExt : SimplePersistentEnvExtension (Name × ProjectionFunctionInfo) (NameMap ProjectionFunctionInfo) := arbitrary _
@[export lean_add_projection_info]
def addProjectionFnInfo (env : Environment) (projName : Name) (ctorName : Name) (nparams : Nat) (i : Nat) (fromClass : Bool) : Environment :=
@ -40,14 +40,14 @@ namespace Environment
def getProjectionFnInfo (env : Environment) (projName : Name) : Option ProjectionFunctionInfo :=
match env.getModuleIdxFor projName with
| some modIdx =>
match (projectionFnInfoExt.getModuleEntries env modIdx).binSearch (projName, default _) (fun a b => Name.quickLt a.1 b.1) with
match (projectionFnInfoExt.getModuleEntries env modIdx).binSearch (projName, arbitrary _) (fun a b => Name.quickLt a.1 b.1) with
| some e => some e.2
| none => none
| none => (projectionFnInfoExt.getState env).find projName
def isProjectionFn (env : Environment) (n : Name) : Bool :=
match env.getModuleIdxFor n with
| some modIdx => (projectionFnInfoExt.getModuleEntries env modIdx).binSearchContains (n, default _) (fun a b => Name.quickLt a.1 b.1)
| some modIdx => (projectionFnInfoExt.getModuleEntries env modIdx).binSearchContains (n, arbitrary _) (fun a b => Name.quickLt a.1 b.1)
| none => (projectionFnInfoExt.getState env).contains n
end Environment

2
library/Init/Lean/ReducibilityAttrs.lean
View file

@ -20,7 +20,7 @@ registerEnumAttributes `reducibility
(`irreducible, "irreducible", ReducibilityStatus.irreducible)]
@[init mkReducibilityAttrs]
constant reducibilityAttrs : EnumAttributes ReducibilityStatus := default _
constant reducibilityAttrs : EnumAttributes ReducibilityStatus := arbitrary _
@[export lean_get_reducibility_status]
def getReducibilityStatus (env : Environment) (n : Name) : ReducibilityStatus :=

4
library/Init/Lean/Runtime.lean
View file

@ -9,10 +9,10 @@ import Init.Core
namespace Lean
@[extern "lean_closure_max_args"]
constant closureMaxArgsFn : Unit → Nat := default _
constant closureMaxArgsFn : Unit → Nat := arbitrary _
@[extern "lean_max_small_nat"]
constant maxSmallNatFn : Unit → Nat := default _
constant maxSmallNatFn : Unit → Nat := arbitrary _
def closureMaxArgs : Nat :=
closureMaxArgsFn ()

2
library/Init/Lean/Scopes.lean
View file

@ -39,7 +39,7 @@ registerSimplePersistentEnvExtension {
}
@[init regScopeManagerExtension]
constant scopeManagerExt : SimplePersistentEnvExtension Name ScopeManagerState := default _
constant scopeManagerExt : SimplePersistentEnvExtension Name ScopeManagerState := arbitrary _
namespace Environment

10
library/Init/Lean/TypeClass/Synth.lean
View file

@ -27,7 +27,7 @@ instance TypedExpr.HasToString : HasToString TypedExpr :=
⟨λ ⟨val, type⟩ => "TypedExpr(" ++ toString val ++ ", " ++ toString type ++ ")"⟩
instance TypedExpr.Inhabited : Inhabited TypedExpr :=
⟨⟨default _, default _⟩⟩
⟨⟨arbitrary _, arbitrary _⟩⟩
structure Node : Type :=
(anormSubgoal : Expr)
@ -35,13 +35,13 @@ structure Node : Type :=
(futureAnswer : TypedExpr)
instance Node.Inhabited : Inhabited Node :=
⟨⟨default _, {}, default _⟩⟩
⟨⟨arbitrary _, {}, arbitrary _⟩⟩
structure ConsumerNode extends Node :=
(remainingSubgoals : List Expr)
instance ConsumerNode.Inhabited : Inhabited ConsumerNode :=
⟨⟨default _, default _⟩⟩
⟨⟨arbitrary _, arbitrary _⟩⟩
inductive Waiter : Type
| consumerNode : ConsumerNode → Waiter
@ -56,7 +56,7 @@ structure GeneratorNode extends Node :=
(remainingInstances : List Instance)
instance GeneratorNode.Inhabited : Inhabited GeneratorNode :=
⟨⟨default _, default _⟩⟩
⟨⟨arbitrary _, arbitrary _⟩⟩
structure TableEntry : Type :=
(waiters : Array Waiter)
@ -65,7 +65,7 @@ structure TableEntry : Type :=
structure TCState : Type :=
(env : Environment)
(finalAnswer : Option TypedExpr := none)
(mainMVar : Expr := default _)
(mainMVar : Expr := arbitrary _)
(generatorStack : Stack GeneratorNode := Stack.empty)
(consumerStack : Stack ConsumerNode := Stack.empty)
(resumeQueue : Queue (ConsumerNode × TypedExpr) := Queue.empty)

44
library/Init/System/IO.lean
View file

@ -60,10 +60,10 @@ match fn.run () with
end
@[extern "lean_io_timeit"]
constant timeit {α : Type} (msg : @& String) (fn : IO α) : IO α := default _
constant timeit {α : Type} (msg : @& String) (fn : IO α) : IO α := arbitrary _
@[extern "lean_io_allocprof"]
constant allocprof {α : Type} (msg : @& String) (fn : IO α) : IO α := default _
constant allocprof {α : Type} (msg : @& String) (fn : IO α) : IO α := arbitrary _
/- Programs can execute IO actions during initialization that occurs before
the `main` function is executed. The attribute `[init <action>]` specifies
@ -71,7 +71,7 @@ constant allocprof {α : Type} (msg : @& String) (fn : IO α) : IO α := default
The action `initializing` returns `true` iff it is invoked during initialization. -/
@[extern "lean_io_initializing"]
constant IO.initializing : IO Bool := default _
constant IO.initializing : IO Bool := arbitrary _
abbrev monadIO (m : Type → Type) := HasMonadLiftT IO m
@ -101,35 +101,35 @@ open Fs
| Sum.inr b => pure b
@[extern "lean_io_prim_put_str"]
constant putStr (s: @& String) : IO Unit := default _
constant putStr (s: @& String) : IO Unit := arbitrary _
@[extern "lean_io_prim_read_text_file"]
constant readTextFile (s : @& String) : IO String := default _
constant readTextFile (s : @& String) : IO String := arbitrary _
@[extern "lean_io_prim_get_line"]
constant getLine : IO String := default _
constant getLine : IO String := arbitrary _
@[extern "lean_io_prim_handle_mk"]
constant handle.mk (s : @& String) (m : Mode) (bin : Bool := false) : IO handle := default _
constant handle.mk (s : @& String) (m : Mode) (bin : Bool := false) : IO handle := arbitrary _
@[extern "lean_io_prim_handle_is_eof"]
constant handle.isEof (h : @& handle) : IO Bool := default _
constant handle.isEof (h : @& handle) : IO Bool := arbitrary _
@[extern "lean_io_prim_handle_flush"]
constant handle.flush (h : @& handle) : IO Unit := default _
constant handle.flush (h : @& handle) : IO Unit := arbitrary _
@[extern "lean_io_prim_handle_close"]
constant handle.close (h : @& handle) : IO Unit := default _
constant handle.close (h : @& handle) : IO Unit := arbitrary _
-- TODO: replace `String` with byte buffer
-- constant handle.read : handle → Nat → EIO String
-- constant handle.write : handle → String → EIO Unit
@[extern "lean_io_prim_handle_get_line"]
constant handle.getLine (h : @& handle) : IO String := default _
constant handle.getLine (h : @& handle) : IO String := arbitrary _
@[extern "lean_io_getenv"]
constant getEnv (var : @& String) : IO (Option String) := default _
constant getEnv (var : @& String) : IO (Option String) := arbitrary _
@[extern "lean_io_realpath"]
constant realPath (fname : String) : IO String := default _
constant realPath (fname : String) : IO String := arbitrary _
@[extern "lean_io_is_dir"]
constant isDir (fname : @& String) : IO Bool := default _
constant isDir (fname : @& String) : IO Bool := arbitrary _
@[extern "lean_io_file_exists"]
constant fileExists (fname : @& String) : IO Bool := default _
constant fileExists (fname : @& String) : IO Bool := arbitrary _
@[extern "lean_io_app_dir"]
constant appPath : IO String := default _
constant appPath : IO String := arbitrary _
@[inline] def liftIO {m : Type → Type} {α : Type} [monadIO m] (x : IO α) : m α :=
monadLift x
@ -235,21 +235,21 @@ end Proc
/- References -/
constant RefPointed (α : Type) : PointedType := default _
constant RefPointed (α : Type) : PointedType := arbitrary _
def Ref (α : Type) : Type := (RefPointed α).type
instance (α : Type) : Inhabited (Ref α) := ⟨(RefPointed α).val⟩
namespace Prim
@[extern "lean_io_mk_ref"]
constant mkRef {α : Type} (a : α) : IO (Ref α) := default _
constant mkRef {α : Type} (a : α) : IO (Ref α) := arbitrary _
@[extern "lean_io_ref_get"]
constant Ref.get {α : Type} (r : @& Ref α) : IO α := default _
constant Ref.get {α : Type} (r : @& Ref α) : IO α := arbitrary _
@[extern "lean_io_ref_set"]
constant Ref.set {α : Type} (r : @& Ref α) (a : α) : IO Unit := default _
constant Ref.set {α : Type} (r : @& Ref α) (a : α) : IO Unit := arbitrary _
@[extern "lean_io_ref_swap"]
constant Ref.swap {α : Type} (r : @& Ref α) (a : α) : IO α := default _
constant Ref.swap {α : Type} (r : @& Ref α) (a : α) : IO α := arbitrary _
@[extern "lean_io_ref_reset"]
constant Ref.reset {α : Type} (r : @& Ref α) : IO Unit := default _
constant Ref.reset {α : Type} (r : @& Ref α) : IO Unit := arbitrary _
end Prim
section

6
library/Init/System/Platform.lean
View file

@ -10,13 +10,13 @@ namespace System
namespace Platform
@[extern "lean_system_platform_nbits"]
constant getNumBits : Unit → Nat := default _
constant getNumBits : Unit → Nat := arbitrary _
@[extern "lean_system_platform_windows"]
constant getIsWindows : Unit → Bool := default _
constant getIsWindows : Unit → Bool := arbitrary _
@[extern "lean_system_platform_osx"]
constant getIsOSX : Unit → Bool := default _
constant getIsOSX : Unit → Bool := arbitrary _
def numBits : Nat := getNumBits ()
def isWindows : Bool := getIsWindows ()

4
library/Init/Util.lean
View file

@ -23,10 +23,10 @@ def dbgSleep {α : Type u} (ms : UInt32) (f : Unit → α) : α :=
f ()
@[extern c inline "#4"]
unsafe def unsafeCast {α : Type u} {β : Type v} [Inhabited β] (a : α) : β := default _
unsafe def unsafeCast {α : Type u} {β : Type v} [Inhabited β] (a : α) : β := arbitrary _
@[neverExtract, extern c inline "lean_panic_fn(#3)"]
constant panic {α : Type u} [Inhabited α] (msg : String) : α := default _
constant panic {α : Type u} [Inhabited α] (msg : String) : α := arbitrary _
@[neverExtract]
def panicWithPos {α : Type u} [Inhabited α] (modName : String) (line col : Nat) (msg : String) : α :=