jroesch

# Licensed to the Apache Software Foundation (ASF) under one
# or more contributor license agreements.  See the NOTICE file
# distributed with this work for additional information
# regarding copyright ownership.  The ASF licenses this file
# to you under the Apache License, Version 2.0 (the
# "License"); you may not use this file except in compliance
# with the License.  You may obtain a copy of the License at
#
#   http://www.apache.org/licenses/LICENSE-2.0
#

jroesch

-- imagine pseudo terms like this
-- def id : Pi (A : Type), A -> A := ...

-- irrelevant.fun 
irrelevant.fun A Type (fun x, x)

-- irrelevant.fun A Type (fun x, x) => fun x, x

-- application of id
(irrelevant.app (fun x, x) A) 10

jroesch

definition position := nat

inductive result (I : Type) : Type -> Type
| fail : Π {R}, I -> list string -> string -> result R
| partial : Π {R}, (I -> result R) -> result R
| done : Π {R}, I -> R -> result R

open result

definition result.map {A B I : Type} (f : A → B) : result I A -> result I B

jroesch

-- module 
structure Map :=
  (M : Type -> Type)
  (K : Type)
  (V : Type)
  (read : K -> V)
  (insert : K -> V -> M K V -> M K V)
  
-- where refinement
definition int_map := { map | map.M = nat }

jroesch

Keybase proof

I hereby claim:

• I am jroesch on github.
• I am jroesch (https://keybase.io/jroesch) on keybase.
• I have a public key ASBf8b_8AaIUVF36T9XaBWbFXAx5x4EKks0ER_dErpVcWwo

To claim this, I am signing this object:

jroesch

import system.IO
import system.ffi
-- import config

-- This is all just config
set_option native.library_path "/Users/jroesch/Git/lean/build/debug"
set_option native.include_path "/Users/jroesch/Git/lean/src"
-- This flag controls whether lean will automatically invoke C++
-- set_option native.compile false
set_option native.emit_dwarf true

jroesch

inductive induction_target :=
| expr : expr -> induction_target
| name : name → induction_target

definition expr_to_induction_target [coercion] (e : expr) : induction_target :=
  induction_target.expr e

definition name_to_induction_target [coercion] (n : name) : induction_target :=
  induction_target.name n

jroesch

#include <iostream>
#include "util/numerics/mpz.h"
#include "library/vm/vm_io.h"
#include "library/vm/vm.h"
#include "init/init.h"

namespace lean {
lean::vm_obj put_nat(lean::vm_obj const &, lean::vm_obj const &);
}

jroesch

check @nat.rec

constant C : nat -> Type
constant cZ : C nat.zero
constant cS : forall n, C n -> C (nat.succ n)

eval (@nat.rec C cZ cS nat.zero)

constant x : nat

jroesch

We couldn’t find that file to show.